closes #33

src/CubicalHott/Theorem2-7-2.agda

@@ -0,0 +1,55 @@
+{-# OPTIONS --cubical #-}
+
+module CubicalHott.Theorem2-7-2 where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Data.Sigma
+
+theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
+  → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
+theorem {P = P} {w = w} {w' = w'} =
+  isoToEquiv (iso f g fg gf) where
+    f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w'))
+    f x = cong fst x , cong snd x
+
+    g : Σ (fst w ≡ fst w') (λ p → PathP (λ i → P (p i)) (snd w) (snd w')) → w ≡ w'
+    g x i = fst x i , snd x i
+
+    fg : section f g
+    fg b = refl
+
+    gf : retract f g
+    gf b = refl
+
+
+-- theorem : {A : Type} {P : A → Type} {w w' : Σ A P}
+--   → (w ≡ w') ≃ Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
+-- theorem {P = P} {w = w} {w' = w'} =
+--   isoToEquiv (iso f g {!   !} {!   !}) where
+--     f : w ≡ w' → Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w')
+--     f = J (λ y' p' → Σ (fst w ≡ fst y') (λ q → subst P q (snd w) ≡ snd y'))
+--       (refl , transportRefl (snd w))
+--       -- subst P (λ _ → fst w) (snd w) ≡ w .snd
+--     -- x = (λ i → fst (x i)) , J (λ y' p' → {!   !}) {!   !} x where
+--       -- subst P (λ i → fst (x i)) (snd w) ≡ snd w'
+--       -- P (fst w')
+--       -- ———— Boundary (wanted) —————————————————————————————————————
+--       -- i = i0 ⊢ transp (λ i₁ → P (fst (x i₁))) i0 (snd w)
+--       -- i = i1 ⊢ snd w'
+
+--     g : Σ (fst w ≡ fst w') (λ p → subst P p (snd w) ≡ snd w') → w ≡ w'
+--     g x i = fst x i , {!   !}
+--     -- helper i where
+--       -- helper : PathP (λ i → P (fst x i)) (snd w) (snd w')
+--       -- helper i =
+--       --   let u = λ j → λ where
+--       --     (i = i0) → {!   !}
+--       --     (i = i1) → {!   !}
+--       --   -- let u = λ j → λ where
+--       --   --   (i = i0) → transportRefl (snd w) j
+--       --   --   (i = i1) → snd w'
+--       --   in hcomp u {! snd x ? !}
+
+