Getting to terms with Lift and Setω, and variable occurrences in expressions

Question

In a previous question, I had types for a toy language

data Type : Set where
  Nat  : Type
  Prp : Type

I thought about interpreting them by using a disjoint union Type → Set ⊎ Set₁, but thought level lifiting would be best and was helped to obtain

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

Now suppose my toy language has variables and expressions

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

Then semantics of expressions,

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₁ ⟧ₑ σ))

I kind of get that in-general lift (lower x) ≠ x due to 'level refreshing' due to lift, but still why cannot the last line simply be ⟦ e ⟧ₑ σ ≡ ⟦ e₁ ⟧ₑ σ ?

I must admit that this is my first time using Lift and sadly did not find a tutorial/explanation on it ---besides the idea that it embeds small types into large types, as indicated by its definition.

---

Since I've everything laid out, let me make a rather particular query.

With the standard/derived equalities,

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

I can defined textual substitution over expressions,

_[_/_] : ∀ {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 ]

Now is the issue of variable occurrences within expressions.

_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 ⟧ₑ σ

I've had trouble using either definition. In particular, I could not even define one in terms of the other. Any help on this would be appreciated!

---

After some digging around, I tried

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

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

However, now I get Setω errors for the definition of State above! That is,

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

As far as I know, such an error occurs, roughly, when one has an assignment of levels to universes.

What shenanigans am I unsconsciously doing to get this trouble?

Answer 1

Recall that Set₁ ∋ Lift ℕ ∋ ⟦ e ⟧ₑ σ and Set α ∋ (Set α ∋ A ∋ x) ≡ (Set α ∋ A ∋ y), where _∋_ is from the Function module:

infixl 0 _∋_
_∋_ : ∀ {a} (A : Set a) → A → A
A ∋ x = x

Hence the expression ⟦ e ⟧ₑ σ ≡ ⟦ e₁ ⟧ₑ σ lies in Set₁ (because the types of ⟦ e ⟧ₑ σ and ⟦ e₁ ⟧ₑ σ lie in Set₁), while you need it to be in Set. You can either write

⟦_⟧ₑ (e ≈ e₁) σ = lower (⟦ e ⟧ₑ σ) ≡ lower (⟦ e₁ ⟧ₑ σ)

or redefine _≡_ making use of a new feature that allows to "force out" levels that appear only in the types of parameters and indices of a data type:

data _≡′_ {a} {A : Set a} (x : A) : A → Set where
  refl′ : x ≡′ x

Note the Set instead of Set a. Then it's

⟦_⟧ₑ (e ≈ e₁) σ = ⟦ e ⟧ₑ σ ≡′ ⟦ e₁ ⟧ₑ σ

I'll choose the first option.

---

Your _not-occurs-inₙ_ are not quite not-occurs, since e can be Var v and E [ v / Var v ] ≡ E regardless of whether v occurs in E or not. Why not define _not-occurs-in_ as a data type? BTW, I think it would be more standard to pronounce substitutions either as E [ v ≔ e ] or [ e / v ] E.

You can go from _not-occurs-in₀_ to _not-occurs-in₁_ like this:

+-inj : ∀ {E₁ E₂ E₃ E₄} -> E₁ + E₂ ≡ E₃ + E₄ -> E₁ ≡ E₃ × E₂ ≡ E₄ 
+-inj refl = refl , refl

≈-inj : ∀ {E₁ E₂ E₃ E₄} -> E₁ ≈ E₂ ≡ E₃ ≈ E₄ -> E₁ ≡ E₃ × E₂ ≡ E₄ 
≈-inj refl = refl , refl

coe : ∀ {t s} {v : Variable t} → (E : Expr s) → v not-occurs-in₀ E → v not-occurs-in₁ E
coe {t} {v} (Var w)  q {e} rewrite q {e} = refl
coe ( n)  q = refl
coe ( p)  q = refl
coe (E + E₁) q =
  cong₂ (λ n m → lift $ lower n +ℕ lower m) (coe E (proj₁ (+-inj q))) (coe E₁ (proj₂ (+-inj q)))
coe (E ≈ E₁) q =
  cong₂ (λ p₁ p₂ → lower p₁ ≡ lower p₂) (coe E (proj₁ (≈-inj q))) (coe E₁ (proj₂ (≈-inj q)))

---

It's not possible to give a name to a type like ∀ α -> Set (f α) because this type doesn't have a type in Agda as explained in the link you mentioned. But you can transform the expression a little to get a function:

F : ∀ α -> Set (suc (f α))
F α = Set (f α)

Using the same transformation you can define NState and ⟦_⟧ₑ:

NState : ∀ t → Set (levelOf t)
NState t = Variable t → New⟦ t ⟧ₜ

⟦_⟧ₑ : ∀ {t} → Expr t → (∀ {t} -> NState t) → New⟦ t ⟧ₜ
⟦_⟧ₑ (Var v)  σ = σ v
⟦_⟧ₑ ( q)   σ = q
⟦_⟧ₑ ( p)   σ = p
⟦_⟧ₑ (e + e₁) σ = ⟦ e ⟧ₑ σ +ℕ ⟦ e₁ ⟧ₑ σ
⟦_⟧ₑ (e ≈ e₁) σ = ⟦ e ⟧ₑ σ ≡ ⟦ e₁ ⟧ₑ σ

Try to go from the current NState to your original NState to see the issue with the latter: what is the type of ∀ {t} -> NState t? Set applied to what? The type of NState t depends on t, but when t is universally quantified this dependency can't be reflected at the type level.

It would be nice to write

syntax (∀ {t} -> NState t) = State

but Agda doesn't allow that.

BTW, in theory a universe of universes (i.e. Setω) exists: it's a super universe. Though, Setω is an unfortunate name for it, because such universe is not a Set — it's bigger than any Set, because it contains them all. You can found these ideas expressed in Agda here.

The code.