school/type-theory
2
0
Fork 0
Code Issues 11 Pull requests Actions Packages Projects 1 Releases Wiki Activity

wip 2.7.4

Browse source
This commit is contained in:
Michael Zhang 2024-07-21 14:45:33 -05:00
parent fabb22e855
commit 61dc53cf32
1 changed files with 11 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/HottBook/Chapter2.lagda.md
View file

@ -589,14 +589,17 @@ corollary2∙7∙3 z = refl
### Theorem 2.7.4
```
-- theorem2∙7∙4 : {A : Set} {P : A → Set}
-- → (Q : Σ A (λ x → P x) → Set)
-- → {x y : A}
-- → (p : x ≡ y)
-- → (u z : Σ (P x) (λ u → Q (x , u)))
-- → transport (λ x → Σ (Σ (P x) λ u → Q (x , u)) λ _ → Σ (P x) λ u → Q (x , u)) p (u , z)
-- ≡ ( transport (λ x → Σ (P x) λ u → Q (x , u)) p u
-- , transport (λ (m , n) → {! Σ (P y) ? !}) (Σ-≡ (p , refl)) z)
-- module theorem2∙7∙4 where
-- private
-- TF = λ P Q x → Σ (P x) (λ u → Q (x , u))
-- theorem2∙7∙4 : {A : Set} {P : A → Set}
-- → (Q : Σ A P → Set)
-- → {x y : A}
-- → (p : x ≡ y)
-- → (u z : Σ (P x) (λ u → Q (x , u)))
-- → transport (λ r → Σ {! !} {! !}) p (u , z) ≡ (transport {! !} p u , transport {! TF P Q !} (pair-≡ (p , refl)) z)
-- theorem2∙7∙4 Q refl u z = refl
```
## 2.8 The unit type