From 61dc53cf32d6cef4364e51c0fa4717b3d6687010 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sun, 21 Jul 2024 14:45:33 -0500 Subject: [PATCH] wip 2.7.4 --- src/HottBook/Chapter2.lagda.md | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/src/HottBook/Chapter2.lagda.md b/src/HottBook/Chapter2.lagda.md index 73fe35a..8d3e521 100644 --- a/src/HottBook/Chapter2.lagda.md +++ b/src/HottBook/Chapter2.lagda.md @@ -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