110 lines
5.3 KiB
Markdown
110 lines
5.3 KiB
Markdown
```
|
||
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. (currently only pi 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 [ γ ]
|
||
|
||
Welcome to intensionality hell.
|
||
|
||
```
|
||
app-subst-pathp : {Δ Γ : Ob} (γ : Hom Δ Γ) {A : ∣ Ty Γ ∣} {B : ∣ Ty (Γ ; A) ∣}
|
||
(f : ∣ Tr Γ (∏ A B) ∣) (x : ∣ Tr Γ A ∣)
|
||
→ B ⟦ ⟨ γ ∘∘ p , q ⟩ ⟧ ⟦ ⟨id, x [ γ ] ⟩ ⟧
|
||
≡ B ⟦ ⟨id, x ⟩ ⟧ ⟦ γ ⟧
|
||
app-subst-pathp {Δ} {Γ} γ {A} {B} f x =
|
||
B ⟦ ⟨ γ ∘∘ p , q ⟩ ⟧ ⟦ ⟨id, x [ γ ] ⟩ ⟧
|
||
≡˘⟨ ⟦⟧-compose ⟨ γ ∘∘ p , q ⟩ ⟨id, x [ γ ] ⟩ B ⟩
|
||
B ⟦ ⟨ γ ∘∘ p , q ⟩ ∘ ⟨id, x [ γ ] ⟩ ⟧
|
||
≡⟨⟩
|
||
B ⟦ ⟨ γ ∘ p , transport (λ i → ⟦⟧-tr-comp γ p A (~ i)) q ⟩ ∘ ⟨id, x [ γ ] ⟩ ⟧
|
||
≡⟨ (λ i → B ⟦ ⟨⟩-∘ ⟨id, x [ γ ] ⟩ (γ ∘ p) A (transport (λ i → ⟦⟧-tr-comp γ (p {Δ} {A ⟦ γ ⟧}) A (~ i)) q) i ⟧) ⟩
|
||
B ⟦ ⟨ (γ ∘ p) ∘ ⟨id, x [ γ ] ⟩ , transport (λ i → ⟦⟧-tr-comp (γ ∘ p) ⟨id, x [ γ ] ⟩ A (~ i))
|
||
(transport (λ j → ⟦⟧-tr-comp γ (p {Δ} {A ⟦ γ ⟧}) A (~ j)) q [ ⟨id, x [ γ ] ⟩ ]) ⟩ ⟧
|
||
≡⟨ ((λ i → B ⟦ ⟨ assoc γ p ⟨id, x [ γ ] ⟩ (~ i) , {! !} ⟩ ⟧)) ⟩
|
||
B ⟦ ⟨ γ ∘ (p ∘ ⟨id, x [ γ ] ⟩) , transport (λ i → ⟦⟧-tr-comp γ (p ∘ ⟨id, x [ γ ] ⟩) A (~ i))
|
||
(transport (λ j → ⟦⟧-tr-comp p ⟨id, x [ γ ] ⟩ (A ⟦ γ ⟧) (~ j)) (q [ ⟨id, x [ γ ] ⟩ ])) ⟩ ⟧
|
||
≡⟨⟩
|
||
B ⟦ ⟨ γ ∘∘ p ∘ ⟨id, x [ γ ] ⟩ , transport (λ i → ⟦⟧-tr-comp p ⟨id, x [ γ ] ⟩ (A ⟦ γ ⟧) (~ i)) (q [ ⟨id, x [ γ ] ⟩ ]) ⟩ ⟧
|
||
≡⟨ (λ i → B ⟦ ⟨ γ ∘∘ p-∘ id (transport (λ i → ⟦⟧-tr-id (A ⟦ γ ⟧) (~ i)) (x [ γ ])) i , {! !} ⟩ ⟧) ⟩
|
||
B ⟦ ⟨ γ ∘∘ id , transport (λ i → ⟦⟧-tr-id (A ⟦ γ ⟧) (~ i)) (x [ γ ]) ⟩ ⟧
|
||
≡⟨⟩
|
||
B ⟦ ⟨ γ ∘ id , transport (λ i → ⟦⟧-tr-comp γ id A (~ i)) (transport (λ j → ⟦⟧-tr-id (A ⟦ γ ⟧) (~ j)) (x [ γ ])) ⟩ ⟧
|
||
≡⟨ {! !} ⟩
|
||
B ⟦ ⟨ γ ∘ id , transport ((λ j → ⟦⟧-tr-id (A ⟦ γ ⟧) (~ j)) ∙ (λ i → ⟦⟧-tr-comp γ id A (~ i))) (x [ γ ]) ⟩ ⟧
|
||
≡⟨ {! !} ⟩
|
||
B ⟦ ⟨ γ , x [ γ ] ⟩ ⟧
|
||
≡⟨ {! !} ⟩
|
||
B ⟦ ⟨ id ∘∘ γ , transport (λ i → ∣ Tr Δ (⟦⟧-id A (~ i) ⟦ γ ⟧) ∣) (x [ γ ]) ⟩ ⟧
|
||
≡⟨ {! !} ⟩
|
||
B ⟦ ⟨id, x ⟩ ⟧ ⟦ γ ⟧
|
||
∎
|
||
|
||
|
||
field
|
||
app-subst : {Δ Γ : Ob} (γ : Hom Δ Γ) {A : ∣ Ty Γ ∣} {B : ∣ Ty (Γ ; A) ∣}
|
||
(f : ∣ Tr Γ (∏ A B) ∣) (x : ∣ Tr Γ A ∣)
|
||
→ PathP (λ i → ∣ Tr Δ (app-subst-pathp γ f x (~ i)) ∣ )
|
||
(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 ⟩ ]
|
||
```
|
||
|