CwF 的結構與規範

學習 https://github.com/martinescardo/TypeTopology/pull/434 中的 CwF 部分

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

open import MLTT.Spartan
open import UF.Base

CwF 的基本結構

record CwFStructure : (𝓤 ⊔ 𝓥)⁺ ̇ where
  field

有一個 Contexts 構成的範疇（Category of contexts）

這個範疇的元素是 contexts
關於 context Γ 跟 context Δ 我們可以討論他們的 morphism Sub Γ Δ，叫做 substitution
每個 context Γ 都有自己到自己的 morphism，也就是 identity
如果有兩個 substitutions 有合適的 type，我們就能把它們串起來
Contexts 範疇有 terminal object，就是空的 context ε

    Con : 𝓤 ̇
    Sub : Con → Con → 𝓥 ̇
    idSub : {Γ : Con} → Sub Γ Γ
    _○_ : {Γ Δ Θ : Con} → Sub Δ Θ → Sub Γ Δ → Sub Γ Θ

    ε : Con
    εSub : {Γ : Con} → Sub Γ ε

有一系列 indexed by context 的 collection 叫做 Ty，表示 types
每個 morphism 都給出了 type 逆變

    -- Type functor
    Ty : Con → 𝓤 ̇
    _[_] : {Γ Δ : Con} → Ty Γ → Sub Δ Γ → Ty Δ

有一系列 indexed by context A 跟 Ty A 的 collection 叫做 Tm，表示 terms
每個 morphism 都給出了 term 逆變

    -- Term functor
    Tm : (Γ : Con) → Ty Γ → 𝓥 ̇
    _⁅_⁆ : {Γ Δ : Con} {A : Ty Γ} → Tm Γ A → (σ : Sub Δ Γ) → Tm Δ (A [ σ ])

我們可以擴充手上的 context

如果我們有一個 context Γ 跟一個 type T 我們可以得到 Γ, T，一個基於原本 context 擴充的新 context

    _₊_ : (Γ : Con) → Ty Γ → Con

如果有一個 Sub Δ Γ，那每個 term u ∈ Tm Δ (A [ σ ]) 都教了我們要怎麼建立從 Δ 到 Γ 的擴充 Γ, u : A 的 morphism

    ⟨_,_⟩ : {Γ Δ : Con} {A : Ty Γ}
          → (σ : Sub Δ Γ) → Tm Δ (A [ σ ]) → Sub Δ (Γ ₊ A)

我們總是能從 Γ, A 取出 Γ 部分

    p : {Γ : Con} {A : Ty Γ} → Sub (Γ ₊ A) Γ

我們總是能從 Γ, u : A 取出 u 這個 term，類型取 A [ p ]

    q : {Γ : Con} {A : Ty Γ} → Tm (Γ ₊ A) (A [ p ])

CwF 的 laws

CwF 不只是結構，還需要滿足一些互動上的 laws，才能合理的排除掉並不能解釋 type theory 的那些範疇

record CwFLaws {𝓤 : Universe} {𝓥 : Universe}
  (S : CwFStructure {𝓤} {𝓥})
  : (𝓤 ⊔ 𝓥)⁺ ̇ where
  open CwFStructure S
  field

identity substitution 跟任何 substitution σ 結合都是 σ（當然前提是可以結合的那些）

    idl : {Γ Δ : Con} {σ : Sub Γ Δ}
        → idSub ○ σ ＝ σ
    idr : {Γ Δ : Con} {σ : Sub Γ Δ}
        → σ ○ idSub ＝ σ

要求結合有 associativity

    ○-assoc : {Γ Δ Θ Ξ : Con} {σ : Sub Θ Ξ} {τ : Sub Δ Θ} {ρ : Sub Γ Δ}
            → (σ ○ τ) ○ ρ ＝ σ ○ (τ ○ ρ)

要求去 empty context 的 substitution 是唯一的。這是因為具體的 contexts 中我們觀察到這件事一定成立，但對很多範疇來說這並不成立，因此 CwF 定義這點就能消除大量無意義的 models

    εSub-unique : {Γ : Con} {σ : Sub Γ ε}
                → σ ＝ εSub

Type A 經過 identity substitution 應該不變
對 type 的替換與 context morphism 的組合具有交換性

    ty[id] : {Γ : Con} {A : Ty Γ}
           → A [ idSub ] ＝ A
    ty[○]  : {Γ Δ Θ : Con} {A : Ty Γ} {σ : Sub Δ Γ} {τ : Sub Θ Δ}
           → A [ σ ○ τ ] ＝ A [ σ ] [ τ ]

Term t 經過 identity substitution 應該不變
對 term 的替換與 context morphism 的組合具有交換性（需要連帶考慮 type 的變化）

    tm[id] : {Γ : Con} {A : Ty Γ} {t : Tm Γ A}
           → transport (Tm Γ) ty[id]
             (t ⁅ idSub ⁆) ＝ t
    tm[○] : {Γ Δ Θ : Con} {A : Ty Γ} {t : Tm Γ A} {σ : Sub Δ Γ} {τ : Sub Θ Δ}
           → transport (Tm Θ) ty[○]
             (t ⁅ σ ○ τ ⁆) ＝ t ⁅ σ ⁆ ⁅ τ ⁆

這邊是 type/term substitution 跟 context extension 之間的關係，其實翻譯成實際上的使用都是一些很直覺的規範

    p,-β : {Γ Δ : Con} {A : Ty Γ} {σ : Sub Δ Γ} {t : Tm Δ (A [ σ ])}
         → p ○ ⟨ σ , t ⟩ ＝ σ
    q,-β : {Γ Δ : Con} {A : Ty Γ} {σ : Sub Δ Γ} {t : Tm Δ (A [ σ ])}
         → transport (Tm Δ) {(A [ p ]) [ ⟨ σ , t ⟩ ]} (ty[○] ⁻¹ ∙ ap (A [_]) p,-β)
          (q ⁅ ⟨ σ , t ⟩ ⁆) ＝ t
    p,q-η : {Γ Δ : Con} {A : Ty Γ} {σ : Sub Δ Γ} {t : Tm Δ (A [ σ ])}
          → ⟨ p , q ⟩ ＝ idSub {Γ ₊ A}
    ,○-distrib : {Γ Δ Θ : Con} {A : Ty Γ} {σ : Sub Δ Γ} {t : Tm Δ (A [ σ ])} {τ : Sub Θ Δ}
               → ⟨ σ , t ⟩ ○ τ ＝ ⟨ σ ○ τ , transport (Tm Θ) {(A [ σ ]) [ τ ]} {A [ σ ○ τ ]} (ty[○] ⁻¹)
                                           (t ⁅ τ ⁆) ⟩

最後把 structure 跟 laws 兩個接在一起

record CwF : (𝓤 ⊔ 𝓥)⁺ ̇ where
  field
    structure : CwFStructure {𝓤} {𝓥}
    laws : CwFLaws structure

  open CwFStructure structure public
  open CwFLaws laws public