Разбираемся с Lift и Setω и вхождениями переменных в выражения

В предыдущем вопросе у меня были типы для игрушечного языка

data Type : Set where
  Nat  : Type
  Prp : Type

Я думал интерпретировать их, используя непересекающийся союз Type → Set ⊎ Set₁, но подумал, что лучше всего будет поднять уровень, и мне помогли получить

⟦_⟧ₜ : Type → Set₁
⟦ Nat ⟧ₜ = Lift ℕ
⟦ Prp ⟧ₜ = Set

Теперь предположим, что в моем игрушечном языке есть переменные и выражения.

data Variable : Type → Set where
  x y : ∀ {t} → Variable t

data Expr : Type → Set₁ where
  Var : ∀ {t} (v : Variable t) → Expr t      -- varaible symbols
  ???? : ℕ → Expr Nat                         -- constant symbols
  ???? : Set → Expr Prp
  _+_ : (m n : Expr Nat) → Expr Nat          -- binary function symbol
  _≈_ : (e f : Expr Nat) → Expr Prp          -- binary relation symbol

Затем семантика выражений,

State = ∀ {t} → Variable t → ⟦ t ⟧ₜ

⟦_⟧ₑ : ∀ {t} → Expr t → State → ⟦ t ⟧ₜ
⟦_⟧ₑ (Var v)  σ = σ v
⟦_⟧ₑ (???? q)   σ = lift q
⟦_⟧ₑ (???? p)   σ = p
⟦_⟧ₑ (e + e₁) σ = lift $ lower (⟦ e ⟧ₑ σ) +ℕ     lower (⟦ e₁ ⟧ₑ σ)
⟦_⟧ₑ (e ≈ e₁) σ = lift (lower (⟦ e ⟧ₑ σ)) ≡ lift (lower (⟦ e₁ ⟧ₑ σ))

Я как бы понимаю, что в целом lift (lower x) ≠ x из-за «обновления уровня» из-за lift, но все же, почему последняя строка не может быть просто ⟦ e ⟧ₑ σ ≡ ⟦ e₁ ⟧ₑ σ ?

Я должен признать, что это мой первый раз, когда я использую Lift и, к сожалению, не нашел учебника/объяснения по нему --- кроме идеи, что он встраивает маленькие типы в большие типы, как указано в его определении.

Поскольку я все изложил, позвольте мне задать довольно специфический вопрос.

Со стандартными/производными равенствами

-- no quick `deriving Eq' mechanism, yet.
postulate _≟ₜ_ : Decidable {A = Type} _≡_   
postulate _≟ᵥ_ : ∀ {t s} → Variable t → Variable s → Bool

Я могу определить текстовую замену выражений,

_[_/_] : ∀ {s t} → Expr t → Variable s → Expr s → Expr t
_[_/_] {s} {t} (Var v) u e with s ≟ₜ t
Var v [ u / e ] | yes refl = if v ≟ᵥ u then e else Var v
Var v [ u / e ] | no ¬p = Var v
???? n [ v / e ] = ???? n
???? p [ v / e ] = ???? p
(E + F) [ v / e ] = E [ v / e ] + F [ v / e ]
(E ≈ F) [ v / e ] = E [ v / e ] ≈ F [ v / e ]

Теперь вопрос о вхождениях переменных в выражения.

_not-occurs-in₀_ : ∀ {t} → Variable t → Expr t → Set₁
v not-occurs-in₀ E = ∀ {e} → E [ v / e ] ≡ E

_not-occurs-in₁_ : ∀ {t} → Variable t → Expr t → Set₁
v not-occurs-in₁ E = ∀ {e} {σ : State} → ⟦ E [ v / e ] ⟧ₑ σ ≡ ⟦ E ⟧ₑ σ

У меня были проблемы с использованием любого определения. В частности, я не мог даже определить одно через другое. Любая помощь в этом будет оценена по достоинству!

После некоторых копаний я попытался

levelOf : Type → Level
levelOf Nat = zero
levelOf Prp = suc zero

New⟦_⟧ₜ : (t : Type) → Set (levelOf t)
New⟦ Nat ⟧ₜ = ℕ
New⟦ Prp ⟧ₜ = Set    

Однако теперь я получаю Setω ошибок для определения State выше! То есть,

-- works fine if i use the risky {-# OPTIONS --type-in-type #-}
NState = {t : Type} → Variable t → New⟦ {!t!} ⟧ₜ

Насколько я знаю, возникает такая ошибка , грубо говоря, когда есть присвоение уровней вселенным.

Какие махинации я бессознательно делаю, чтобы получить эту проблему?