univalence in product-category step1

src/Cat/Category/Product.agda

@@ -214,32 +214,10 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
           × PathP (λ i → ℂ.Arrow (p i) B) xb yb
           )
       step1
-        = (λ{ (p , x)
-          → (ℂ.idToIso _ _ p)
-          , let
-             P-l : (p : X ≡ Y) → Set _
-             P-l φ = PathP (λ i → ℂ.Arrow (φ i) A) xa ya
-             P-r : (p : X ≡ Y) → Set _
-             P-r φ = PathP (λ i → ℂ.Arrow (φ i) B) xb yb
-             left  : P-l p
-             left = fst x
-             right : P-r p
-             right = snd x
-           in subst {P = P-l} iso-id-inv left , subst {P = P-r} iso-id-inv right
-          })
-        -- Goal is:
-        --
-        --     φ x
-        --
-        -- where `x` is
-        --
-        --   ℂ.isoToId (ℂ.idToIso _ _ p)
-        --
-        -- I have `φ p` in scope, but surely `p` and `x` are the same - though
-        -- perhaps not definitonally.
-        , (λ{ (iso , x) → ℂ.isoToId iso , x})
-        , funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) {!!}})
-        , funExt (λ x → Σ≡ (sym id-iso-inv) {!!})
+        = symIso
+            (isoSigFst {A = (X ℂ.≅ Y)} {B = (X ≡ Y)} {!!} {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb)} ℂ.isoToId
+                           (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd))
+
       step2
         : Σ (X ℂ.≅ Y) (λ iso
           → let p = ℂ.isoToId iso

src/Cat/Equivalence.agda

@@ -39,6 +39,23 @@ module _ {ℓa ℓb : Level} where
   _≅_ : Set ℓa → Set ℓb → Set _
   A ≅ B = Σ (A → B) Isomorphism
 
+symIso : ∀ {ℓa ℓb} {A : Set ℓa}{B : Set ℓb} → A ≅ B → B ≅ A
+symIso (f , g , p , q)= g , f , q , p
+
+module _ {ℓa ℓb ℓc} {A : Set ℓa} {B : Set ℓb} (sB : isSet B) {Q : B → Set ℓc} (f : A → B)  where
+
+  Σ-fst-map : Σ A (\ a → Q (f a)) → Σ B Q
+  Σ-fst-map (x , q) = f x , q
+
+  isoSigFst : Isomorphism f → Σ A (\ a → Q (f a)) ≅ (Σ B Q)
+  isoSigFst (g , g-f , f-g) = Σ-fst-map
+    , (\ { (b , q) → g b , transp (\ i → Q (f-g (~ i) b)) q })
+    , funExt (\ { (a , q) → Cat.Prelude.Σ≡ (\ i → g-f i a)
+             let r = (transp-iso' ((λ i → Q (f-g (i) (f a)))) q) in
+                 transp (\ i → PathP (\ j → Q (sB _ _ (λ j₁ → f-g j₁ (f a)) (λ j₁ → f (g-f j₁ a)) i j)) (transp (λ i₁ → Q (f-g (~ i₁) (f a))) q) q) r })
+    , funExt (\ { (b , q) → Cat.Prelude.Σ≡ (\ i → f-g i b) (transp-iso' (λ i → Q (f-g i b)) q)})
+
+
 module _ {ℓ : Level} {A B : Set ℓ} {f : A → B}
   (g : B → A) (s : {A B : Set ℓ} → isSet (A → B)) where