cwfs/src/CwF/Structures.lagda.md

open import Cat.Prelude
open import CwF.Base

module CwF.Structures where

This file defines several additional structures a CwF might have, such as pi types, universes, sigma types, and identity types.

First are pi types, because a type theory without them are pretty uninteresting.

record has-Pi {o h f : _} {𝓒 : Precategory o h}
              (cwf : is-CwF {o} {h} {f} 𝓒) : Type (lsuc (o ⊔ h ⊔ f)) where
  open Precategory 𝓒
  open is-CwF cwf
  field

The type formation rule for pi types is straight forward.

    ∏ : {Γ : Ob} (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣) → ∣ Ty Γ ∣

Likewise, the introduction rule is what one would expect.

    Cλ : {Γ : Ob} (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣) (b : ∣ Tr (Γ ; A) B ∣)
       → ∣ Tr Γ (∏ A B) ∣

Application also needs to be introduced.

    app : {Γ : Ob} {A : ∣ Ty Γ ∣} {B : ∣ Ty (Γ ; A) ∣} (f : ∣ Tr Γ (∏ A B) ∣)
          (x : ∣ Tr Γ A ∣) → ∣ Tr Γ (B ⟦ ⟨id, x ⟩ ⟧ ) ∣

Substitution must also be closed under all of these.

    ∏-subst : {Δ Γ : Ob} (γ : Hom Δ Γ) (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣)
            → ∏ A B ⟦ γ ⟧ 
            ≡ ∏ (A ⟦ γ ⟧) (B ⟦ ⟨ γ ∘∘ p , q ⟩ ⟧)

    Cλ-subst : {Δ Γ : Ob} (γ : Hom Δ Γ) (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣) 
               (b : ∣ Tr (Γ ; A) B ∣)
             → PathP (λ i → ∣ Tr Δ (∏-subst γ A B i) ∣)
                     (Cλ A B b [ γ ])
                     (Cλ (A ⟦ γ ⟧) (B ⟦ ⟨ γ ∘∘ p , q ⟩ ⟧) (b [ ⟨ γ ∘∘ p , q ⟩ ]))

There's quite a hefty pathp here...
typeof app (transport (λ i → ∣ Tr Δ (∏-subst γ A B i) ∣) (f [ γ ])) (x [ γ ])
B ⟦ ⟨ γ  ∘ p , q ⟩ ⟧ ⟦ ⟨id, x [ γ ] ⟩ ⟧
B ⟦ ⟨ γ  ∘ p , q ⟩ ∘ ⟨id, x [ γ ] ⟩ ⟧
B ⟦ ⟨ γ  ∘ p ∘ ⟨id, x [ γ ] ⟩, q [ ⟨id, x [ γ ] ⟩ ] ⟩ ⟧
B ⟦ ⟨ γ  ∘ id, x [ γ ] ⟩ ⟧
B ⟦ ⟨ id ∘ γ , x [ γ ] ⟩ ⟧
B ⟦ ⟨ id, x ⟩ ⟧ ⟦ γ ⟧
typeof app f x [ γ ]

    app-subst : {Δ Γ : Ob} (γ : Hom Δ Γ) {A : ∣ Ty Γ ∣} {B : ∣ Ty (Γ ; A) ∣} 
                (f : ∣ Tr Γ (∏ A B) ∣) (x : ∣ Tr Γ A ∣) 
              → PathP {!   !}
                      (app f x [ γ ])
                      (app (transport (λ i → ∣ Tr Δ (∏-subst γ A B i) ∣) (f [ γ ])) (x [ γ ]))

Lastly comes the star of the show, \beta reduction.

    Cβ : {Γ : Ob} (A : ∣ Ty Γ ∣) (B : ∣ Ty (Γ ; A) ∣) (b : ∣ Tr (Γ ; A) B ∣)
         (a : ∣ Tr Γ A ∣)
       → app (Cλ A B b) a ≡ b [ ⟨id, a ⟩ ]