Substitution extension by a type

Given $Δ ⊢ 𝛾 : Γ$ and $Γ ⊢ 𝐴$ , we can define the extension $𝛾 . 𝐴$ of $𝛾$ by $𝐴$ as

Δ . 𝐴 [𝛾] ⊢ 𝛾 . 𝐴 = (𝛾 \circ 𝐩) . 𝐪 : Γ . 𝐴 .

with the derivation

Δ ⊢ 𝛾 : Γ Δ ⊢ 𝐴 [𝛾] Δ . 𝐴 [𝛾] ⊢ 𝐩 Γ, 𝐴 [𝛾] : Δ Δ . 𝐴 [𝛾] ⊢ 𝛾 \circ 𝐩 Γ, 𝐴 [𝛾] : Γ Γ ⊢ 𝐴 Δ ⊢ 𝛾 : Γ Γ ⊢ 𝐴 Δ ⊢ 𝐴 [𝛾] Δ . 𝐴 [𝛾] ⊢ 𝐪 Γ, 𝐴 [𝛾] : 𝐴 [𝛾 \circ 𝐩] (V) Δ . 𝐴 [𝛾] ⊢ (𝛾 \circ 𝐩 Γ, 𝐴 [𝛾]) . 𝐪 Γ, 𝐴 [𝛾] : Γ . 𝐴 (E)

Properties

The following are derivable:

$Ξ ⊢ 𝛿 : Δ Δ ⊢ 𝛾 : Γ Ξ ⊢ 𝑎 : 𝐴 [𝛾 \circ 𝛿] Ξ ⊢ 𝛾 . 𝐴 \circ 𝛿 . 𝑎 = (𝛾 \circ 𝛿) . 𝑎 : Γ . 𝐴 (\Rightarrow)$
$Ξ ⊢ 𝛿 : Δ Δ ⊢ 𝛾 : Γ Γ ⊢ 𝐴 Ξ . 𝐴 [𝛾 \circ 𝛿] ⊢ 𝛾 . 𝐴 \circ 𝛿 . 𝐴 [𝛾] = (𝛾 \circ 𝛿) . 𝐴 : Γ . 𝐴 (\Rightarrow)$
$Γ ⊢ 𝐴 Γ . 𝐴 ⊢ 𝐢 𝐝 . 𝐴 = 𝐢 𝐝 : Γ . 𝐴 (\Rightarrow)$

Proof of 1–3

For ^P1, expanding definitions and using ^P2 gives

𝛾 . 𝐴 \circ 𝛿 . 𝑎 = (𝛾 \circ 𝐩) . 𝐪 \circ 𝛿 . 𝑎 = (𝛾 \circ 𝐩 \circ 𝛿 . 𝑎) . 𝐪 [𝛿 . 𝑎] = (𝛾 \circ 𝛿) . 𝑎

completing the proof of ^P1.

Applying this result to ^P2 gives

𝛾 . 𝐴 \circ 𝛿 . 𝐴 [𝛾] = 𝛾 . 𝐴 \circ (𝛿 \circ 𝐩) . 𝐪 = (𝛾 \circ 𝛿 \circ 𝐩) . 𝐪 = (𝛾 \circ 𝛿) . 𝐴

proving ^P2.

For ^P3 we have $𝐢 𝐝 . 𝐴 = (𝐢 𝐝 \circ 𝐩) . 𝐪 = 𝐩 . 𝐪 = (𝐩 \circ 𝐢 𝐝) . 𝐪 [𝐢 𝐝] = 𝐢 𝐝$ by $𝜂 𝐩 𝐪$ .

#state/tidy | #lang/en | #SemBr