diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index e1cd33d..9e51447 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -327,6 +327,7 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
       asTypeIso : TypeIsomorphism (idToIso A B)
       asTypeIso = toIso _ _ univalent
 
+      -- FIXME Rename
       inverse-from-to-iso' : AreInverses (idToIso A B) isoToId
       inverse-from-to-iso' = snd iso
 
@@ -377,6 +378,62 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         where
         lem : p~ <<< p* ≡ identity
         lem = fst (snd (snd (idToIso _ _ p)))
+    module _ {A B X : Object} (iso : A ≅ B) where
+      private
+        p : A ≡ B
+        p = isoToId iso
+        p-dom : Arrow A X ≡ Arrow B X
+        p-dom = cong (λ x → Arrow x X) p
+        p-cod : Arrow X A ≡ Arrow X B
+        p-cod = cong (λ x → Arrow X x) p
+        lem : ∀ {A B} {x : A ≅ B} → idToIso A B (isoToId x) ≡ x
+        lem {x = x} i = snd inverse-from-to-iso' i x
+
+      open Σ iso renaming (fst to ι) using ()
+      open Σ (snd iso) renaming (fst to ι~ ; snd to inv)
+
+      coe-dom : {f : Arrow A X} → coe p-dom f ≡ f <<< ι~
+      coe-dom {f} = begin
+        coe p-dom f
+          ≡⟨ 9-1-9 p refl f ⟩
+        fst (idToIso _ _ refl) <<< f <<< fst (snd (idToIso _ _ p))
+          ≡⟨ cong (λ φ → φ <<< f <<< fst (snd (idToIso _ _ p))) subst-neutral ⟩
+        identity <<< f <<< fst (snd (idToIso _ _ p))
+          ≡⟨ cong (λ φ → identity <<< f <<< φ) (cong (λ x → (fst (snd x))) lem) ⟩
+        identity <<< f <<< ι~
+          ≡⟨ cong (_<<< ι~) leftIdentity ⟩
+        f <<< ι~ ∎
+
+      coe-cod : {f : Arrow X A} → coe p-cod f ≡ ι <<< f
+      coe-cod {f} = begin
+        coe p-cod f
+          ≡⟨ 9-1-9 refl p f ⟩
+        fst (idToIso _ _ p) <<< f <<< fst (snd (idToIso _ _ refl))
+          ≡⟨ cong (λ φ → fst (idToIso _ _ p) <<< f <<< φ) subst-neutral ⟩
+        fst (idToIso _ _ p) <<< f <<< identity
+          ≡⟨ cong (λ φ → φ <<< f <<< identity) (cong fst lem) ⟩
+        ι <<< f <<< identity
+          ≡⟨ sym isAssociative ⟩
+        ι <<< (f <<< identity)
+          ≡⟨ cong (ι <<<_) rightIdentity ⟩
+        ι <<< f ∎
+
+      module _ {f : Arrow A X} {g : Arrow B X} (q : PathP (λ i → p-dom i) f g) where
+        domain-twist : g ≡ f <<< ι~
+        domain-twist = begin
+          g            ≡⟨ sym (coe-lem q) ⟩
+          coe p-dom f  ≡⟨ coe-dom ⟩
+          f <<< ι~      ∎
+
+        -- This can probably also just be obtained from the above my taking the
+        -- symmetric isomorphism.
+        domain-twist0 : f ≡ g <<< ι
+        domain-twist0 = begin
+          f ≡⟨ sym rightIdentity ⟩
+          f <<< identity ≡⟨ cong (f <<<_) (sym (fst inv)) ⟩
+          f <<< (ι~ <<< ι) ≡⟨ isAssociative ⟩
+          f <<< ι~ <<< ι ≡⟨ cong (_<<< ι) (sym domain-twist) ⟩
+          g <<< ι ∎
 
     -- | All projections are propositions.
     module Propositionality where
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 4a318cb..8a91642 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -238,7 +238,7 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         -- 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) (toPathP {A = λ i → {!!}} {!!})})
+        , funExt (λ{ (p , q , r) → Σ≡ (sym iso-id-inv) {!!}})
         , funExt (λ x → Σ≡ (sym id-iso-inv) {!!})
       step2
         : Σ (X ℂ.≅ Y) (λ iso
@@ -249,55 +249,9 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
           )
         ≈ ((X , xa , xb) ≅ (Y , ya , yb))
       step2
-        = ( λ{ ((f , f~ , inv-f) , p , q)
-            →
-            let
-              r : X ≡ Y
-              r = ℂ.isoToId (f , f~ , inv-f)
-              r-arrow : (ℂ.Arrow X A) ≡ (ℂ.Arrow Y A)
-              r-arrow i = ℂ.Arrow (r i) A
-              t : coe r-arrow xa ≡ ℂ.identity ℂ.<<< xa ℂ.<<< f~
-              t = {!? ≡ ?!}
-              lem : ∀ {A B} {x : A ℂ.≅ B} → ℂ.idToIso A B (ℂ.isoToId x) ≡ 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 ≡⟨ 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 ⟩
-                ℂ.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  , (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 , {!!})
+        = ( λ{ (iso@(f , f~ , inv-f) , p , q)
+            → ( f  , sym (ℂ.domain-twist0 iso p) , sym (ℂ.domain-twist0 iso q))
+            , ( f~ , sym (ℂ.domain-twist iso p) , sym (ℂ.domain-twist iso q))
             , lemA (fst inv-f)
             , lemA (snd inv-f)
             }
@@ -308,26 +262,26 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
             iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
             p : X ≡ Y
             p = ℂ.isoToId iso
-            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 , ? , {!!}})
+            pA : ℂ.Arrow X A ≡ ℂ.Arrow Y A
+            pA = cong (λ x → ℂ.Arrow x A) p
+            pB : ℂ.Arrow X B ≡ ℂ.Arrow Y B
+            pB = cong (λ x → ℂ.Arrow x B) p
+            k0 = begin
+              coe pB xb ≡⟨ ℂ.coe-dom iso ⟩
+              xb ℂ.<<< fst f~ ≡⟨ snd (snd f~) ⟩
+              yb ∎
+            k1 = begin
+              coe pA xa ≡⟨ ℂ.coe-dom iso ⟩
+              xa ℂ.<<< fst f~ ≡⟨ fst (snd f~) ⟩
+              ya ∎
+            helper : PathP (λ i → pA i) xa ya
+            helper = coe-lem-inv k1
+          in iso , coe-lem-inv k1 , coe-lem-inv k0})
         , record
           { fst = funExt (λ x → lemSig
             (λ x → propSig prop0 (λ _ → prop1))
             _ _
-            (Σ≡ {!ℂ!} (ℂ.propIsomorphism _ _ _)))
+            (Σ≡ {!!} (ℂ.propIsomorphism _ _ _)))
           ; snd = funExt (λ{ (f , _) → lemSig propIsomorphism _ _ {!refl!}})
           }
           where