Export TypeIsomorphism as an alias for Equivalence.Isomorphism

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

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)

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)

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