data Ty : Set where
* : Ty
_⇒_ : (a b : Ty) → Ty
data Cxt : Set where
ε : Cxt
_,_ : (Γ : Cxt) (a : Ty) → Cxt
infixr 4 _⇒_
infixl 2 _,_
mutual
data Var : (Γ : Cxt) (a : Ty) → Set where
vz : ∀{Γ a} → Var (Γ , a) a
vs : ∀{Γ a b} (x : Var Γ a) → Var (Γ , b) a
data Nf (Γ : Cxt) : (a : Ty) → Set where
var : ∀{a b} (x : Var Γ a) (S : Spine Γ a b) → Nf Γ b
abs : ∀{a b} (t : Nf (Γ , a) b) → Nf Γ (a ⇒ b)
data Spine (Γ : Cxt) : (a b : Ty) → Set where
ε : ∀{a} → Spine Γ a a
_∙_ : ∀{a b c} (u : Nf Γ a) (S : Spine Γ b c) → Spine Γ (a ⇒ b) c
appendSpine : ∀{Γ a b c} → Spine Γ a b → Spine Γ b c → Spine Γ a c
appendSpine ε T = T
appendSpine (u ∙ S) T = u ∙ appendSpine S T
Ren : (Δ Γ : Cxt) → Set
Ren Δ Γ = ∀{a} → Var Γ a → Var Δ a
liftR : ∀{Γ Δ b} (ρ : Ren Δ Γ) → Ren (Δ , b) (Γ , b)
liftR ρ vz = vz
liftR ρ (vs x) = vs (ρ x)
mutual
ren : ∀{Γ Δ b} (ρ : Ren Δ Γ) (t : Nf Γ b) → Nf Δ b
ren ρ (var x S) = var (ρ x) (renSpine ρ S)
ren ρ (abs t) = abs (ren (liftR ρ) t)
renSpine : ∀{Γ Δ a b} (ρ : Ren Δ Γ) (S : Spine Γ a b) → Spine Δ a b
renSpine ρ ε = ε
renSpine ρ (u ∙ S) = ren ρ u ∙ renSpine ρ S
wk : ∀{Γ a b} → Nf Γ b → Nf (Γ , a) b
wk = ren vs
data Sub a : (Δ Γ : Cxt) → Set where
sg : ∀{Γ} (u : Nf Γ a) → Sub a Γ (Γ , a)
lift : ∀{Δ Γ b} (σ : Sub a Δ Γ) → Sub a (Δ , b) (Γ , b)
data Res a Δ : (b : Ty) → Set where
var : ∀{b} (x : Var Δ b) → Res a Δ b
tm : (u : Nf Δ a) → Res a Δ a
wkRes : ∀{Δ a b c} → Res a Δ b → Res a (Δ , c) b
wkRes (var x) = var (vs x)
wkRes (tm u) = tm (wk u)
lookup : ∀{Δ Γ a b} (σ : Sub a Δ Γ) (x : Var Γ b) → Res a Δ b
lookup (sg u) vz = tm u
lookup (sg u) (vs x) = var x
lookup (lift σ) vz = var vz
lookup (lift σ) (vs x) = wkRes (lookup σ x)
mutual
hsubst : ∀{Γ Δ a b} (σ : Sub a Δ Γ) (t : Nf Γ b) → Nf Δ b
hsubst σ (var x S) = rapps (lookup σ x) (hsubsts σ S)
hsubst σ (abs t) = abs (hsubst (lift σ) t)
hsubsts : ∀{Γ Δ a b c} (σ : Sub a Δ Γ) (S : Spine Γ b c) → Spine Δ b c
hsubsts σ ε = ε
hsubsts σ (u ∙ S) = hsubst σ u ∙ hsubsts σ S
rapps : ∀ {Δ a b c} → Res a Δ b → Spine Δ b c → Nf Δ c
rapps (var x) S = var x S
rapps (tm t) S = apps t S
apps : ∀{Γ a b} (t : Nf Γ a) (S : Spine Γ a b) → Nf Γ b
apps t ε = t
apps (var x S) T = var x (appendSpine S T)
apps (abs t) (u ∙ S) = apps (hsubst (sg u) t) S
appNf : ∀{Γ a b} → (t : Nf Γ (a ⇒ b)) (u : Nf Γ a) → Nf Γ b
appNf t u = apps t (u ∙ ε)
data Tm (Γ : Cxt) : (a : Ty) → Set where
var : ∀{a} (x : Var Γ a) → Tm Γ a
abs : ∀{a b} (t : Tm (Γ , a) b) → Tm Γ (a ⇒ b)
app : ∀{a b} (t : Tm Γ (a ⇒ b)) (u : Tm Γ a) → Tm Γ b
nf : ∀{Γ a} → Tm Γ a → Nf Γ a
nf (var x) = var x ε
nf (abs t) = abs (nf t)
nf (app t u) = appNf (nf t) (nf u)