基於 CwF 的結構與規範 現在可以討論 CwF 最常被拿出來講的案例
{-# OPTIONS --safe --without-K #-} open import MLTT.Spartan open import ag-T2O7 module ag-A3OG {𝓤 : Universe} where
open CwFStructure open CwFLaws open CwF str : CwFStructure str .Con = 𝓤 ̇ str .Sub Γ Δ = Γ → Δ str .idSub = id str ._○_ = _∘_ str .ε = 𝟙 str .εSub _ = ⋆ str .Ty Γ = Γ → 𝓤 ̇ str ._[_] A σ x = A (σ x) str .Tm Γ A = (x : Γ) → A x str ._⁅_⁆ t σ x = t (σ x) str ._₊_ Γ A = Σ x ꞉ Γ , A x str .⟨_,_⟩ σ t δ = σ δ , t δ str .p = pr₁ str .q = pr₂ law : CwFLaws str law .idl = refl law .idr = refl law .○-assoc = refl law .εSub-unique = refl law .ty[id] = refl law .ty[○] = refl law .tm[id] = refl law .tm[○] = refl law .p,-β = refl law .q,-β = refl law .p,q-η = refl law .,○-distrib = refl TypeCwF : CwF TypeCwF .structure = str TypeCwF .laws = law