The copy-and-paste approach

{-# OPTIONS --safe --without-K #-}
module ag-000M where

open import MLTT.Spartan

類型跟 context

data Ty : 𝓤₀ ̇ where
  base : Ty
  _⇒_ : Ty → Ty → Ty
infixl 50 _⇒_

data Con : 𝓤₀ ̇ where
  ◇ : Con
  _▷_ : Con → Ty → Con
infixl 40 _▷_

等一下用的變數
de Bruijn variables
terms

variable
  Γ Δ Ξ : Con
  A B C : Ty

data _∋_ : Con → Ty → 𝓤₀ ̇ where
  here : Γ ▷ A ∋ A
  there : Γ ∋ A → (B : Ty)
        ------------------
        → Γ ▷ B ∋ A
infixl 30 _∋_

data _⊢_ : Con → Ty → 𝓤₀ ̇ where
  -- embeds variables in λ-terms
  `_ : Γ ∋ A → Γ ⊢ A
  -- application t · u
  _·_ : Γ ⊢ A ⇒ B → Γ ⊢ A → Γ ⊢ B
  ƛ_ : Γ ▷ A ⊢ B → Γ ⊢ A ⇒ B
infixl 20 _⊢_
infixl 60 `_
infixl 50 _·_
infixl 40 ƛ_

substitution 定義成

data _⊩_ : Con → Con → 𝓤₀ ̇ where
  ε : Γ ⊩ ◇
  _,_ : Γ ⊩ Δ → Γ ⊢ A → Γ ⊩ Δ ▷ A

現在要定義 substitution 在 terms 跟 variables 上的作用：

_v[_] : Δ ∋ A → Γ ⊩ Δ → Γ ⊢ A
here v[ ts , t ] = t
there i B v[ ts , t ] = i v[ ts ]

data _⊩v_ : Con → Con → 𝓤₀ ̇ where
  ε : Γ ⊩v ◇
  _,_ : Γ ⊩v Δ → Γ ∋ A → Γ ⊩v Δ ▷ A

_v[_]v : Γ ∋ A → Δ ⊩v Γ → Δ ∋ A
here v[ is , i ]v = i
there i B v[ is , j ]v = i v[ is ]v

_⁺v_ : Γ ⊩v Δ → (A : Ty) → Γ ▷ A ⊩v Δ
ε ⁺v A = ε
(is , i) ⁺v A = (is ⁺v A) , there i A

_↑v_ : Γ ⊩v Δ → (A : Ty) → Γ ▷ A ⊩v Δ ▷ A
is ↑v A = (is ⁺v A) , here

_[_]v : Γ ⊢ A → Δ ⊩v Γ → Δ ⊢ A
(` i) [ is ]v = ` (i v[ is ]v)
(t · u) [ is ]v = (t [ is ]v) · (u [ is ]v)
(ƛ t) [ is ]v = ƛ (t [ is ↑v _ ]v)

idv : Γ ⊩v Γ
idv {Γ = ◇} = ε
idv {Γ = Γ ▷ A} = idv ↑v A

為了定義下面的 suc-tm，需要定義上面大量的類似結構 Γ ⊩v Δ

_⁺_ : Γ ⊩ Δ → (A : Ty) → Γ ▷ A ⊩ Δ
ε ⁺ A = ε
(ts , t) ⁺ A = (ts ⁺ A) , suc-tm t A
  where
  suc-tm : Γ ⊢ B → (A : Ty) → Γ ▷ A ⊢ B
  suc-tm t A = t [ idv ⁺v A ]v

_↑_ : Γ ⊩ Δ → (A : Ty) → Γ ▷ A ⊩ Δ ▷ A
ts ↑ A = ts ⁺ A , ` here

_[_] : Γ ⊢ A → Δ ⊩ Γ → Δ ⊢ A
(` i) [ ts ] = i v[ ts ]
(t · u) [ ts ] = (t [ ts ]) · (u [ ts ])
(ƛ t) [ ts ] = ƛ (t [ ts ↑ _ ])

The copy-and-paste approach [ag-000M]