n σ A^{σ} n ∈ h_{n}^{σ} :

A^{σ}A^{σ} ψ_{n}^{σ}

h_{n}^{σ} A^{σ} A_{n}^{σ}

h_{n}^{σ}[A^{σ}] h_{n}^{σ}

Γ ≡ x_{1}:σ_{1}, …, x_{k}:σ_{k}

A^{Γ} A^{σ_{1}}× … ×A^{σ_{k}}

h_{n}^{Γ} h_{n}^{σ_{1}}× … ×h_{n}^{σ_{k}} A_{n}^{Γ} h_{n}^{Γ}

Γ (A^{Γ}) =

⋃_{n∈} A_{n}^{Γ} (A^{Γ})

(A^{Γ}) n Γ n ∈ Γ_{n} =

(w_{Γ_{n}}, S_{Γ_{n}}) w_{Γ_{n}}

A_{n}^{Γ}

P ∈ S_{Γ_{n}}

Γ ⊢ M : ι

P = { Γ⊢M^{−1}({i})∩w_{Γ_{n}} | i ∈ }\{∅} .

n Γ_{n} Γ (Γ, Δ)_{n}Γ_{n} : (γ, δ) ↦ γ

Γ_{n} ι Γ ?? n (Γ, Δ)_{n}Γ_{n}

Γ, Δ ⊢

M : ι Γ ⊢ M : ι

σ n ∈ Γ f :

A_{n}^{Γ}A_{n}^{σ} (1)

f ∈

R(A^{σ})Γ_{n}_{n}

(2) f = Γ⊢MA_{n}^{Γ}

Γ ⊢ M : σ σ

S_{Γ_{n}}

R(A^{ι})Γ_{n}_{n} =

R(N)Γ_{n}_{n}

A_{n}^{Γ} ⊥

σ τ στ f :

A_{n}^{Γ}A_{n}^{στ} f ∈

R(A^{στ})Γ_{n}_{n}

∘f∘π_{1}π_{2} ∈ R(A^{τ})(Γ,x:σ)_{n}_{n}

x Γ π_{1} n (Γ, x:σ)_{n}

Γ_{n} π_{2} ∈

R(A^{σ})(Γ,x:σ)_{n}_{n} σ π_{2} Γ, x:σ ⊢ x : σ τ

∘f∘π_{1}π_{2} = Γ, x:σ ⊢ MA_{n}^{Γ,x:σ}

Γ, x:σ ⊢

M : τ

f = Γ ⊢ ψ_{n}^{στ} (λx:σ.M)A_{n}^{Γ}

f = Γ⊢MA_{n}^{Γ}

Γ ⊢ M : στ f ∈

R(A^{στ})Γ_{n}_{n} π : (Γ, Δ)_{n}Γ_{n} n a ∈

R(A^{σ})(Γ,Δ)_{n}_{n} σ Γ, Δ ⊢

N : σ h_{n}^{σ}∘ a = Γ, Δ ⊢NA_{n}^{Γ,Δ}

h_{n}^{σ}∘ a :