Modified verion of 9.1.9

src/Cat/Category.agda

@@ -337,6 +337,8 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       private
         q* : Arrow b b'
         q* = fst (idToIso b b' q)
+        p* : Arrow a a'
+        p* = fst (idToIso _ _ p)
         p~ : Arrow a' a
         p~ = fst (snd (idToIso _ _ p))
         pq : Arrow a b ≡ Arrow a' b'
@@ -365,6 +367,17 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       9-1-9 : coe pq f ≡ q* <<< f <<< p~
       9-1-9 = pathJ D d a' p
 
+      9-1-9' : coe pq f <<< p* ≡ q* <<< f
+      9-1-9' = begin
+        coe pq f <<< p* ≡⟨ cong (_<<< p*) 9-1-9 ⟩
+        q* <<< f <<< p~ <<< p* ≡⟨ sym isAssociative ⟩
+        q* <<< f <<< (p~ <<< p*) ≡⟨ cong (λ φ → q* <<< f <<< φ) lem ⟩
+        q* <<< f <<< identity ≡⟨ rightIdentity ⟩
+        q* <<< f ∎
+        where
+        lem : p~ <<< p* ≡ identity
+        lem = fst (snd (snd (idToIso _ _ p)))
+
     -- | All projections are propositions.
     module Propositionality where
       -- | Terminal objects are propositional - a.k.a uniqueness of terminal

src/Cat/Category/Product.agda

@@ -250,11 +250,10 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         ≈ ((X , xa , xb) ≅ (Y , ya , yb))
       step2
         = ( λ{ ((f , f~ , inv-f) , p , q)
-          → ( f , (let r = fromPathP p in {!r!}) , {!!})
-            , ( (f~ , {!!} , {!!})
-              , lemA (fst inv-f)
-              , lemA (snd inv-f)
-              )
+            → ( f  , {!ℂ.9-1-9'!} , {!!})
+            , ( f~ , {!!} , {!!})
+            , lemA (fst inv-f)
+            , lemA (snd inv-f)
             }
           )
         , (λ{ (f , f~ , inv-f , inv-f~) →