From fd18985e53fe90e8ae2e0abc3d67d3d94a4695f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Mon, 9 Apr 2018 18:10:39 +0200
Subject: [PATCH] Export TypeIsomorphism as an alias for
 Equivalence.Isomorphism

---
 src/Cat/Category.agda                 | 10 +++++++---
 src/Cat/Category/Monad.agda           |  3 +++
 src/Cat/Category/Monad/Voevodsky.agda |  3 ---
 src/Cat/Category/Product.agda         |  7 +++++--
 4 files changed, 15 insertions(+), 8 deletions(-)

diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index bb26526..776c92a 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -29,7 +29,11 @@
 module Cat.Category where
 
 open import Cat.Prelude
-open import Cat.Equivalence as Equivalence renaming (_≅_ to _≈_ ; Isomorphism to TypeIsomorphism) hiding (preorder≅)
+import Cat.Equivalence
+open Cat.Equivalence public using () renaming (Isomorphism to TypeIsomorphism)
+open Cat.Equivalence
+  renaming (_≅_ to _≈_)
+  hiding (preorder≅ ; Isomorphism)
 
 import Function
 
@@ -485,7 +489,7 @@ module Opposite {ℓa ℓb : Level} where
       open IsPreCategory isPreCategory
 
       module _ {A B : ℂ.Object} where
-        k : Equivalence.Isomorphism (ℂ.idToIso A B)
+        k : TypeIsomorphism (ℂ.idToIso A B)
         k = toIso _ _ ℂ.univalent
         open Σ k renaming (fst to η ; snd to inv-η)
         open AreInverses inv-η
@@ -537,7 +541,7 @@ module Opposite {ℓa ℓb : Level} where
             x ∎)
           }
 
-        h : Equivalence.Isomorphism (idToIso A B)
+        h : TypeIsomorphism (idToIso A B)
         h = ζ , inv-ζ
 
       isCategory : IsCategory opRaw
diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda
index 387dc75..8ad64fa 100644
--- a/src/Cat/Category/Monad.agda
+++ b/src/Cat/Category/Monad.agda
@@ -209,3 +209,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
   Monoidal≃Kleisli : M.Monad ≃ K.Monad
   Monoidal≃Kleisli = forth , eqv
+
+  Monoidal≡Kleisli : M.Monad ≡ K.Monad
+  Monoidal≡Kleisli = ua (forth , eqv)
diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda
index 3c6bad6..f4dc465 100644
--- a/src/Cat/Category/Monad/Voevodsky.agda
+++ b/src/Cat/Category/Monad/Voevodsky.agda
@@ -172,9 +172,6 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         where
         t' : ((Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
           ≡ §2-3.§2.toMonad
-        cong-d : ∀ {ℓ} {A : Set ℓ} {ℓ'} {B : A → Set ℓ'} {x y : A}
-          → (f : (x : A) → B x) → (eq : x ≡ y) → PathP (\ i → B (eq i)) (f x) (f y)
-        cong-d f p = λ i → f (p i)
         t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) re-ve
         t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure})
           ≡ (§2-fromMonad ∘ §2-3.§2.toMonad)
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 536467b..1985656 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -203,12 +203,15 @@ module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
         : ((X , xa , xb) ≡ (Y , ya , yb))
         ≈ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
       step0
-        = (λ p → (λ i → fst (p i)) , (λ i → fst (snd (p i))) , (λ i → snd (snd (p i))))
-        , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
+        = (λ p → cong fst p , cong-d (fst ⊙ snd) p , cong-d (snd ⊙ snd) p)
+        -- , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
+        , (λ{ (p , q , r) → Σ≡ p λ i → q i , r i})
         , record
           { verso-recto = {!!}
           ; recto-verso = {!!}
           }
+          where
+          open import Function renaming (_∘_ to _⊙_)
       step1
         : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) A) xa ya) × (PathP (λ i → ℂ.Arrow (p i) B) xb yb))
         ≈ Σ (X ℂ.≅ Y) (λ iso