NOTE: Explicit Weakening

在 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，但我沒有試這是什麼清況。

NOTE: Explicit Weakening [ag-000S]

Instantiation

Left identity

Associative