Prove 9.1.9

src/Cat/Category.agda

@@ -342,8 +342,28 @@ module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
         pq : Arrow a b ≡ Arrow a' b'
         pq i = Arrow (p i) (q i)
 
+      U : ∀ b'' → b ≡ b'' → Set _
+      U b'' q' = coe (λ i → Arrow a (q' i)) f ≡ fst (idToIso _ _ q') <<< f <<< (fst (snd (idToIso _ _ refl)))
+      u : coe (λ i → Arrow a b) f ≡ fst (idToIso _ _ refl) <<< f <<< (fst (snd (idToIso _ _ refl)))
+      u = begin
+        coe refl f     ≡⟨ id-coe ⟩
+        f              ≡⟨ sym leftIdentity ⟩
+        identity <<< f ≡⟨ sym rightIdentity ⟩
+        identity <<< f <<< identity ≡⟨ cong (λ φ → identity <<< f <<< φ) lem ⟩
+        identity <<< f <<< (fst (snd (idToIso _ _ refl))) ≡⟨ cong (λ φ → φ <<< f <<< (fst (snd (idToIso _ _ refl)))) lem ⟩
+        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})
+
+      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')))
+
+      d : coe (λ i → Arrow a (q i)) f ≡ fst (idToIso b b' q) <<< f <<< (fst (snd (idToIso _ _ refl)))
+      d = pathJ U u b' q
+
       9-1-9 : coe pq f ≡ q* <<< f <<< p~
-      9-1-9 = transpP {!!} {!!}
+      9-1-9 = pathJ D d a' p
 
     -- | All projections are propositions.
     module Propositionality where

src/Cat/Equivalence.agda

@@ -3,12 +3,11 @@ module Cat.Equivalence where
 
 open import Cubical.Primitives
 open import Cubical.FromStdLib renaming (ℓ-max to _⊔_)
--- FIXME: Don't hide ≃
-open import Cubical.PathPrelude hiding (inverse ; _≃_)
+open import Cubical.PathPrelude hiding (inverse)
 open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
 open import Cubical.GradLemma
 
-open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; _≃_ ; propSig)
+open import Cat.Prelude using (lemPropF ; setPi ; lemSig ; propSet ; Preorder ; equalityIsEquivalence ; propSig ; id-coe)
 
 import Cubical.Univalence as U
 
@@ -289,14 +288,6 @@ preorder≅ ℓ = record
     }
   }
   where
-  module _ {ℓ : Level} {A : Set ℓ} {a : A} where
-    id-coe : coe refl a ≡ a
-    id-coe = begin
-      coe refl a                 ≡⟨⟩
-      pathJ (λ y x → A) _ A refl ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
-      _ ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
-      a ∎
-
   module _ {ℓ : Level} {A B : Set ℓ} {a : A} where
     inv-coe : (p : A ≡ B) → coe (sym p) (coe p a) ≡ a
     inv-coe p =

src/Cat/Prelude.agda

@@ -88,3 +88,11 @@ IsPreorder
   → (_∼_ : Rel A ℓ) -- The relation.
   → Set _
 IsPreorder _~_ = Relation.Binary.IsPreorder _≡_ _~_
+
+module _ {ℓ : Level} {A : Set ℓ} {a : A} where
+  id-coe : coe refl a ≡ a
+  id-coe = begin
+    coe refl a                 ≡⟨⟩
+    pathJ (λ y x → A) _ A refl ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
+    _ ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩
+    a ∎