在 Substitution Without Copy and Paste 結尾也有提過這篇，就來稍微看一下。
Explicit Weakening
{-# OPTIONS --rewriting --no-level-universe #-} module ag-000S where open import MLTT.Spartan hiding (Type; id) {-# BUILTIN REWRITE _＝_ #-} cong₂ : ∀ {A B C : 𝓤 ̇ } (f : A → B → C) {x y u v} → x ＝ y → u ＝ v → f x u ＝ f y v cong₂ f refl refl = refl
data Type : 𝓤₀ ̇ where base : Type _⇒_ : Type → Type → Type infixr 7 _⇒_ variable A B C : Type data Con : 𝓤₀ ̇ where ∅ : Con _▷_ : Con → Type → Con infixl 5 _▷_ variable Γ Δ Θ Ξ : Con data _⊢_ : Con → Type → 𝓤₀ ̇ where • : Γ ▷ A ⊢ A _↑ : (M : Γ ⊢ B) ------------ → Γ ▷ A ⊢ B ƛ_ : (N : Γ ▷ A ⊢ B) → Γ ⊢ A ⇒ B _·_ : (L : Γ ⊢ A ⇒ B) (M : Γ ⊢ A) ----------------------------- → Γ ⊢ B infix 5 ƛ_ infix 4 _⊢_ infixl 7 _·_ variable L M N P Q : Γ ⊢ A data _⊨_ : Con → Con → 𝓤₀ ̇ where id : Δ ⊨ Δ _↑ : (σ : Γ ⊨ Δ) → Γ ▷ A ⊨ Δ _▷_ : (σ : Γ ⊨ Δ) (M : Γ ⊢ A) ------------ → Γ ⊨ Δ ▷ A infix 4 _⊨_ infix 8 _↑ variable σ τ υ : Γ ⊨ Δ pattern △ = _ ▷ _
Instantiation
_[_] : (M : Δ ⊢ A) (σ : Γ ⊨ Δ) → Γ ⊢ A M [ id ] = M M [ σ ↑ ] = (M [ σ ]) ↑ • [ σ ▷ P ] = P (M ↑) [ σ ▷ P ] = M [ σ ] (ƛ M) [ σ @ △ ] = ƛ (M [ σ ↑ ▷ • ]) (L · M) [ σ @ △ ] = L [ σ ] · (M [ σ ]) _⨟_ : (σ : Θ ⊨ Δ) (τ : Γ ⊨ Θ) → Γ ⊨ Δ σ ⨟ id = σ σ ⨟ (τ ↑) = (σ ⨟ τ) ↑ id ⨟ τ @ △ = τ (σ ↑) ⨟ (τ ▷ Q) = σ ⨟ τ (σ ▷ P) ⨟ τ @ △ = (σ ⨟ τ) ▷ (P [ τ ]) infixl 5 _⨟_ [][] : (M : Δ ⊢ A) (σ : Θ ⊨ Δ) (τ : Γ ⊨ Θ) → M [ σ ] [ τ ] ＝ M [ σ ⨟ τ ] [][] M σ id = refl [][] M σ (τ ↑) = ap _↑ ([][] M σ τ) [][] M id (τ ▷ M₁) = refl [][] M (σ ↑) (τ ▷ M₁) = [][] M σ τ [][] • (σ ▷ P) τ@△ = refl [][] (M ↑) (σ ▷ P) τ@△ = [][] M σ τ [][] (ƛ N) σ@△ τ@△ = ap ƛ_ ([][] N (σ ↑ ▷ •) (τ ↑ ▷ •)) [][] (L · M) σ@△ τ@△ = cong₂ _·_ ([][] L σ τ) ([][] M σ τ) {-# REWRITE [][] #-}
Left identity
left-id : (τ : Γ ⊨ Δ) → id ⨟ τ ＝ τ left-id id = refl left-id (τ ↑) = ap _↑ (left-id τ) left-id (τ ▷ Q) = refl {-# REWRITE left-id #-}
Associative
assoc : (σ : Θ ⊨ Δ) (τ : Ξ ⊨ Θ) (υ : Γ ⊨ Ξ) → (σ ⨟ τ) ⨟ υ ＝ σ ⨟ (τ ⨟ υ) assoc σ τ id = refl assoc σ τ (υ ↑) = ap _↑ (assoc σ τ υ) assoc σ id (υ ▷ M) = refl assoc σ (τ ↑) (υ ▷ M) = assoc σ τ υ assoc id (τ ▷ M₁) (υ ▷ M) = refl assoc (σ ↑) (τ ▷ M₁) (υ ▷ M) = assoc σ τ (υ ▷ M) assoc (σ ▷ M₂) (τ ▷ M₁) (υ ▷ M) = cong₂ _▷_ (assoc σ (τ ▷ M₁) (υ ▷ M)) refl {-# REWRITE assoc #-}
下面的案例是本來在 PLFA 中不好做出來，但用這套就很簡單的問題
_[_]₀ : (N : Γ ▷ A ⊢ B) (M : Γ ⊢ A) ------------ → Γ ⊢ B N [ M ]₀ = N [ id ▷ M ] _[_]₁ : (N : Γ ▷ A ▷ B ⊢ C) (M : Γ ⊢ A) ------------ → Γ ▷ B ⊢ C N [ M ]₁ = N [ (id ▷ M) ↑ ▷ • ] double-subst : N [ M ]₁ [ L ]₀ ＝ N [ L ↑ ]₀ [ M ]₀ double-subst = refl commute-subst : N [ M ]₀ [ L ]₀ ＝ N [ L ]₁ [ M [ L ]₀ ]₀ commute-subst = refl
最後也有談到缺點是 identifying when terms are equivalent may become more difficult，但我沒有試這是什麼清況。