Progress on univalence

src/Cat/Category.agda

@@ -356,7 +356,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
           fst (idToIso _ _ refl) <<< f <<< (fst (snd (idToIso _ _ refl))) ∎
           where
           lem : ∀ {x} → PathP (λ _ → Arrow x x) identity (fst (idToIso x x refl))
-        lem = sym (subst-neutral {P = λ x → Arrow x x})
+          lem = sym subst-neutral
 
         D : ∀ a'' → a ≡ a'' → Set _
         D a'' p' = coe (λ i → Arrow (p' i) (q i)) f ≡ fst (idToIso b b' q) <<< f <<< (fst (snd (idToIso _ _ p')))

src/Cat/Category/Product.agda

@@ -258,22 +258,45 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
               r-arrow i = ℂ.Arrow (r i) A
               t : coe r-arrow xa ≡ ℂ.identity ℂ.<<< xa ℂ.<<< f~
               t = {!? ≡ ?!}
-              lem : ∀ {x} → ℂ.idToIso _ _ (ℂ.isoToId x) ≡ x
+              lem : ∀ {A B} {x : A ℂ.≅ B} → ℂ.idToIso A B (ℂ.isoToId x) ≡ x
-              lem {x} i = snd ℂ.inverse-from-to-iso' i x
+              lem = λ{ {x = x} i → snd ℂ.inverse-from-to-iso' i x}
+              lem' : ∀ {A B} {x : A ≡ B} → ℂ.isoToId (ℂ.idToIso _ _ x) ≡ x
+              lem' = λ{ {x = x} i → fst ℂ.inverse-from-to-iso' i x}
               h : ya ≡ xa ℂ.<<< f~
               h = begin
-                ya ≡⟨ {!!} ⟩
+                ya ≡⟨ sym (coe-lem p) ⟩
                 coe r-arrow xa
                   ≡⟨ ℂ.9-1-9 r refl xa ⟩
                 fst (ℂ.idToIso _ _ refl) ℂ.<<< xa ℂ.<<< fst (snd (ℂ.idToIso _ _ r))
-                  ≡⟨ cong (λ φ → φ ℂ.<<< xa ℂ.<<< fst (snd (ℂ.idToIso _ _ r))) (subst-neutral {P = λ x → ℂ.Arrow x x}) ⟩
+                  ≡⟨ cong (λ φ → φ ℂ.<<< xa ℂ.<<< fst (snd (ℂ.idToIso _ _ r))) subst-neutral ⟩
                 ℂ.identity ℂ.<<< xa ℂ.<<< fst (snd (ℂ.idToIso _ _ r))
                   ≡⟨ cong (λ φ → ℂ.identity ℂ.<<< xa ℂ.<<< φ) (cong (λ x → (fst (snd x))) lem) ⟩
                 ℂ.identity ℂ.<<< xa ℂ.<<< f~
                   ≡⟨ cong (ℂ._<<< f~) ℂ.leftIdentity ⟩
                 xa ℂ.<<< f~ ∎
+              complicated : Y ≡ X
+              complicated = (λ z → sym (ℂ.isoToId (f , f~ , inv-f)) z)
             in
-              ( f  , {!h!} , {!!})
+              ( f  , (begin
+                ℂ [ ya ∘ f ] ≡⟨⟩
+                ya ℂ.<<< f   ≡⟨ sym ℂ.leftIdentity ⟩
+                ℂ.identity ℂ.<<< (ya ℂ.<<< f)
+                  ≡⟨ ℂ.isAssociative ⟩
+                ℂ.identity ℂ.<<< ya ℂ.<<< f
+                  ≡⟨ cong (λ φ → φ ℂ.<<< ya ℂ.<<< f) (sym subst-neutral) ⟩
+                fst (ℂ.idToIso _ _ refl) ℂ.<<< ya ℂ.<<< f
+                ≡⟨ cong (λ φ → fst (ℂ.idToIso _ _ refl) ℂ.<<< ya ℂ.<<< φ)
+                  (begin
+                    f ≡⟨ {!cong (λ x → (fst (snd x))) ((lem {x = f~ , f , swap inv-f}))!} ⟩
+                    -- f ≡⟨ cong fst (sym (lem {f , f~ , inv-f})) ⟩
+                    -- fst (     ℂ.idToIso X Y (           ℂ.isoToId (f , f~ , inv-f))) ≡⟨ {!fst inv-f!} ⟩
+                    fst (snd (ℂ.idToIso Y X (λ z → sym (ℂ.isoToId (f , f~ , inv-f)) z))) ∎)
+                 ⟩
+                _ ℂ.<<< ya ℂ.<<< fst (snd (ℂ.idToIso _ _ _))
+                  ≡⟨ sym (ℂ.9-1-9 (sym r) refl ya) ⟩
+                coe (sym r-arrow) ya
+                  ≡⟨ coe-lem (λ i → p (~ i)) ⟩
+                xa ∎) , {!!})
             , ( f~ , sym h , {!!})
             , lemA (fst inv-f)
             , lemA (snd inv-f)
@@ -283,14 +306,28 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
           let
             iso : X ℂ.≅ Y
             iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
-            helper : PathP (λ i → ℂ.Arrow (ℂ.isoToId {!!} i) A) xa ya
+            p : X ≡ Y
-            helper = {!!}
+            p = ℂ.isoToId iso
-          in iso , helper , {!!}})
+            lem : xa ≡ _
+            lem = begin
+              xa ≡⟨ sym (fst (snd f)) ⟩
+              ya ℂ.<<< fst f ≡⟨ sym ℂ.leftIdentity ⟩
+              ℂ.identity ℂ.<<< (ya ℂ.<<< fst f) ≡⟨ ℂ.isAssociative ⟩
+              ℂ.identity ℂ.<<< ya ℂ.<<< fst f ≡⟨ {!sym (ℂ.9-1-9 ? refl ya)!} ⟩
+              _ ℂ.<<< ya ℂ.<<< _ ≡⟨ sym (ℂ.9-1-9 (sym p) refl ya) ⟩
+              coe (λ i → ℂ.Arrow (p (~ i)) A) ya ∎
+            lem0 = begin
+              xa ≡⟨ {!!} ⟩
+              coe _ xa ≡⟨ {!!} ⟩
+              ya ℂ.<<< fst f ∎
+            helper : PathP (λ i → ℂ.Arrow (p i) A) xa ya
+            helper = {!snd f!}
+          in iso , ? , {!!}})
         , record
           { fst = funExt (λ x → lemSig
             (λ x → propSig prop0 (λ _ → prop1))
             _ _
-            (Σ≡ {!!} (ℂ.propIsomorphism _ _ _)))
+            (Σ≡ {!ℂ!} (ℂ.propIsomorphism _ _ _)))
           ; snd = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}})
           }
           where