From 7eac677efb88fdd39f6cbf23f463fff61abd3bb4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Thu, 12 Apr 2018 10:05:02 +0200
Subject: [PATCH] Prove 9.1.9

---
 src/Cat/Category.agda    | 22 +++++++++++++++++++++-
 src/Cat/Equivalence.agda | 13 ++-----------
 src/Cat/Prelude.agda     |  8 ++++++++
 3 files changed, 31 insertions(+), 12 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 7a764f9..e2c79dc 100644
--- a/src/Cat/Category.agda
+++ b/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
diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda
index 27e77e5..9a36a52 100644
--- a/src/Cat/Equivalence.agda
+++ b/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 =
diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda
index a3d34a4..409549c 100644
--- a/src/Cat/Prelude.agda
+++ b/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 ∎