Lambda calculus (GAT) [ag-0006]

{-# OPTIONS --safe --without-K #-}
module ag-0006 where

open import MLTT.Spartan hiding (_∘_; id)

作者這邊開始解釋從二階理論得出一階理論（GAT）的標準過程

record first-order-lambda-calculus : 𝓤₁ ̇  where
  field
    Con : 𝓤₀ ̇
    Sub : Con → Con → 𝓤₀ ̇

有 terminal object 的 category

    _∘_ : {Δ Γ Θ : Con} → Sub Δ Γ → Sub Θ Δ → Sub Θ Γ
    assoc : {A B C D : Con} {γ : Sub C D} {δ : Sub B C} {θ : Sub A B}
      → (γ ∘ δ) ∘ θ ＝ γ ∘ (δ ∘ θ)
    id : {Γ : Con} → Sub Γ Γ
    id-left : {A B : Con} {γ : Sub A B} → id ∘ γ ＝ γ
    id-right : {A B : Con} {γ : Sub A B} → γ ∘ id ＝ γ
    -- empty context: zero
    ◇ : Con
    ε : {Γ : Con} → Sub Γ ◇
    -- terminal
    ◇η : {Γ : Con} → (σ : Sub Γ ◇) → σ ＝ ε

sort Tm 現在 indexed by Con 且有一個 instantiation operation，這個 operation 是 functorial ([◦], [id]).

    Tm : Con → 𝓤₀ ̇
    _[_] : {Γ Δ : Con} → Tm Γ → Sub Δ Γ → Tm Δ
    [id] : {Γ : Con} {t : Tm Γ} → t [ id ] ＝ t
    [∘] : {Θ Γ Δ : Con} {t : Tm Γ} {γ : Sub Δ Γ} {δ : Sub Θ Δ} → t [ γ ∘ δ ] ＝ t [ γ ] [ δ ]

context extension 讓 contexts 是 natural number algebra

    _▹ : Con → Con

substitutions 是一串 terms，由組成元件表達

    _,,_ : {Δ Γ : Con} → Sub Δ Γ → Tm Δ → Sub Δ (Γ ▹)

有了 contexts 跟 substitutions，變數就可以定義成 De Bruijn indices:

1. 0 = q
2. 1 = q[p]
3. 2 = q[p] [p]，以此類推

    p : {Γ : Con} → Sub (Γ ▹) Γ
    q : {Γ : Con} → Tm (Γ ▹)

應該滿足的等式規則

    ▹β₁ : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm Δ}
      → p ∘ (γ ,, t) ＝ γ
    ▹β₂ : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm Δ}
      → q [ γ ,, t ] ＝ t
    ▹η : {Δ Γ : Con} {σ : Sub Δ (Γ ▹)} → σ ＝ (p ∘ σ ,, q [ σ ])

    lam : {Γ : Con} → Tm (Γ ▹) → Tm Γ
    lam[] : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm (Γ ▹)} → (lam t)[ γ ] ＝ lam (t [ γ ∘ p ,, q ])

    _·_ : {Γ : Con} → Tm Γ → Tm Γ → Tm Γ
    ·[] : {Δ Γ : Con} {γ : Sub Δ Γ} {t u : Tm Γ} → (t · u)[ γ ] ＝ t [ γ ] · (u [ γ ])

    β : {Δ Γ : Con} {γ : Sub Δ Γ} {t : Tm (Γ ▹)} {u : Tm Γ}
      → lam t · u ＝ t [ id ,, u ]

  infixl  _∘_
  infixl  _,,_
  infixl  _·_
  infixl  _[_]