Construct isomorphism from equivalence

Using this somewhat round-about way of constructing an isomorphism from
an equivalence has made typechecking slower in some situations.

E.g. if you're constructing an equivalence from gradLemma and later use
that constructed equivalence to recover the isomorphism, then you
might as well have kept using those functions.

src/Cat/Categories/Sets.agda

@@ -7,22 +7,20 @@ open import Data.Product
 open import Function using (_∘_)
 
 open import Cubical hiding (_≃_ ; inverse)
-open import Cubical.Equivalence
+open import Cubical.Univalence using (univalence ; con ; _≃_)
-  renaming
-    ( _≅_ to _A≅_ )
-  using
-    (_≃_ ; con ; AreInverses)
-open import Cubical.Univalence
 open import Cubical.GradLemma
 
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
 open import Cat.Wishlist
+open import Cat.Equivalence as Eqv using (module NoEta)
+
+module Equivalence = NoEta.Equivalence′
+module Eeq = NoEta
 
 module _ (ℓ : Level) where
   private
-    open import Cubical.Univalence
     open import Cubical.NType.Properties
     open import Cubical.Universe
 
@@ -54,7 +52,7 @@ module _ (ℓ : Level) where
         toIsomorphism : A ≃ B → hA ≅ hB
         toIsomorphism e = obverse , inverse , verso-recto , recto-verso
           where
-          open _≃_ e
+          open Equivalence e
 
         fromIsomorphism : hA ≅ hB → A ≃ B
         fromIsomorphism iso = con obverse (gradLemma obverse inverse recto-verso verso-recto)
@@ -73,8 +71,8 @@ module _ (ℓ : Level) where
           recto-verso b i = proj₂ areInverses i b
 
       private
-        univIso : (A ≡ B) A≅ (A ≃ B)
+        univIso : (A ≡ B) Eqv.≅ (A ≃ B)
-        univIso = _≃_.toIsomorphism univalence
+        univIso = Eeq.toIsomorphism univalence
         obverse' : A ≡ B → A ≃ B
         obverse' = proj₁ univIso
         inverse' : A ≃ B → A ≡ B
@@ -84,31 +82,31 @@ module _ (ℓ : Level) where
         dropP eq i = proj₁ (eq i)
         -- Add proof of being a set to both sides of a set-theoretic equivalence
         -- returning a category-theoretic equivalence.
-        addE : A A≅ B → hA ≅ hB
+        addE : A Eqv.≅ B → hA ≅ hB
         addE eqv = proj₁ eqv , (proj₁ (proj₂ eqv)) , asPair
           where
           areeqv = proj₂ (proj₂ eqv)
           asPair =
-            let module Inv = AreInverses areeqv
+            let module Inv = Eqv.AreInverses areeqv
             in Inv.verso-recto , Inv.recto-verso
 
         obverse : hA ≡ hB → hA ≅ hB
-        obverse = addE ∘ _≃_.toIsomorphism ∘ obverse' ∘ dropP
+        obverse = addE ∘ Eeq.toIsomorphism ∘ obverse' ∘ dropP
 
         -- Drop proof of being a set form both sides of a category-theoretic
         -- equivalence returning a set-theoretic equivalence.
-        dropE : hA ≅ hB → A A≅ B
+        dropE : hA ≅ hB → A Eqv.≅ B
         dropE eqv = obv , inv , asAreInverses
           where
           obv = proj₁ eqv
           inv = proj₁ (proj₂ eqv)
           areEq = proj₂ (proj₂ eqv)
-          asAreInverses : AreInverses A B obv inv
+          asAreInverses : Eqv.AreInverses obv inv
           asAreInverses = record { verso-recto = proj₁ areEq ; recto-verso = proj₂ areEq }
 
-        -- Dunno if this is a thing.
+        isoToEquiv : A Eqv.≅ B → A ≃ B
-        isoToEquiv : A A≅ B → A ≃ B
+        isoToEquiv = Eeq.fromIsomorphism
-        isoToEquiv = {!!}
+
         -- Add proof of being a set to both sides of an equality.
         addP : A ≡ B → hA ≡ hB
         addP p = lemSig (λ X → propPi λ x → propPi (λ y → propIsProp)) hA hB p
@@ -121,23 +119,23 @@ module _ (ℓ : Level) where
         --   )
         -- I can just open them but I wanna be able to see the type annotations.
         verso-recto' : inverse' ∘ obverse' ≡ Function.id
-        verso-recto' = AreInverses.verso-recto (proj₂ (proj₂ univIso))
+        verso-recto' = Eqv.AreInverses.verso-recto (proj₂ (proj₂ univIso))
         recto-verso' : obverse' ∘ inverse' ≡ Function.id
-        recto-verso' = AreInverses.recto-verso (proj₂ (proj₂ univIso))
+        recto-verso' = Eqv.AreInverses.recto-verso (proj₂ (proj₂ univIso))
         verso-recto : (iso : hA ≅ hB) → obverse (inverse iso) ≡ iso
         verso-recto iso = begin
           obverse (inverse iso) ≡⟨⟩
-          ( addE ∘ _≃_.toIsomorphism
+          ( addE ∘ Eeq.toIsomorphism
           ∘ obverse' ∘ dropP ∘ addP
           ∘ inverse' ∘ isoToEquiv
           ∘ dropE) iso
             ≡⟨⟩
-          ( addE ∘ _≃_.toIsomorphism
+          ( addE ∘ Eeq.toIsomorphism
           ∘ obverse'
           ∘ inverse' ∘ isoToEquiv
           ∘ dropE) iso
             ≡⟨ {!!} ⟩ -- obverse' inverse' are inverses
-          ( addE ∘ _≃_.toIsomorphism ∘ isoToEquiv ∘ dropE) iso
+          ( addE ∘ Eeq.toIsomorphism ∘ isoToEquiv ∘ dropE) iso
             ≡⟨ {!!} ⟩ -- should be easy to prove
                       -- _≃_.toIsomorphism ∘ isoToEquiv ≡ id
           (addE ∘ dropE) iso

src/Cat/Category.agda

@@ -144,6 +144,12 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where
 
     Univalent : Set (ℓa ⊔ ℓb)
     Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B)
+    -- Alternative formulation of univalence which is easier to prove in the
+    -- case of the functor category.
+    --
+    --     ∀ A → isContr (Σ[ X ∈ Object ] iso A X)
+
+    -- future work ideas: compile to CAM
 
 -- | The mere proposition of being a category.
 --

src/Cat/Category/Monad/Voevodsky.agda

@@ -18,20 +18,7 @@ open import Cat.Category.Functor as F
 open import Cat.Category.NaturalTransformation
 open import Cat.Category.Monad
 open import Cat.Categories.Fun
-
+open import Cat.Equivalence
--- Utilities
-module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
-  module Equivalence (e : A ≃ B) where
-    obverse : A → B
-    obverse = proj₁ e
-
-    reverse : B → A
-    reverse = inverse e
-
-    -- TODO Implement and push upstream.
-    postulate
-      verso-recto : reverse ∘ obverse ≡ Function.id
-      recto-verso : obverse ∘ reverse ≡ Function.id
 
 module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   private
@@ -42,7 +29,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
     module M = Monoidal ℂ
     module K = Kleisli  ℂ
 
-  module §2-3 (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
+  module §2-3 (omap : Object → Object) (pure : {X : Object} → Arrow X (omap X)) where
     record §1 : Set ℓ where
       open M
 
@@ -149,8 +136,6 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
   -- | to talk about voevodsky's construction.
   module _ (omap : Omap ℂ ℂ) (pure : {X : Object} → Arrow X (omap X)) where
     private
-      -- Could just open this module and rename stuff accordingly, but as
-      -- documentation I will put in the type-annotations here.
       module E = Equivalence (Monoidal≃Kleisli ℂ)
 
       Monoidal→Kleisli : M.Monad → K.Monad

src/Cat/Equivalence.agda

@@ -0,0 +1,183 @@
+{-# OPTIONS --allow-unsolved-metas --cubical #-}
+module Cat.Equivalence where
+
+open import Cubical.Primitives
+open import Cubical.FromStdLib renaming (ℓ-max to _⊔_)
+open import Cubical.PathPrelude hiding (inverse ; _≃_)
+open import Cubical.PathPrelude using (isEquiv ; isContr ; fiber) public
+open import Cubical.GradLemma
+
+module _ {ℓa ℓb : Level} where
+  private
+    ℓ = ℓa ⊔ ℓb
+
+  module _ {A : Set ℓa} {B : Set ℓb} where
+    -- Quasi-inverse in [HoTT] §2.4.6
+    -- FIXME Maybe rename?
+    record AreInverses (f : A → B) (g : B → A) : Set ℓ where
+      field
+        verso-recto : g ∘ f ≡ idFun A
+        recto-verso : f ∘ g ≡ idFun B
+      obverse = f
+      reverse = g
+      inverse = reverse
+
+    Isomorphism : (f : A → B) → Set _
+    Isomorphism f = Σ (B → A) λ g → AreInverses f g
+
+  _≅_ : Set ℓa → Set ℓb → Set _
+  A ≅ B = Σ (A → B) Isomorphism
+
+-- In HoTT they generalize an equivalence to have the following 3 properties:
+module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where
+  record Equiv (iseqv : (A → B) → Set ℓ) : Set (ℓa ⊔ ℓb ⊔ ℓ) where
+    field
+      fromIso      : {f : A → B} → Isomorphism f → iseqv f
+      toIso        : {f : A → B} → iseqv f → Isomorphism f
+      propIsEquiv  : (f : A → B) → isProp (iseqv f)
+
+    -- You're alerady assuming here that we don't need eta-equality on the
+    -- equivalence!
+    _~_ : Set ℓa → Set ℓb → Set _
+    A ~ B = Σ _ iseqv
+
+    fromIsomorphism : A ≅ B → A ~ B
+    fromIsomorphism (f , iso) = f , fromIso iso
+
+    toIsomorphism : A ~ B → A ≅ B
+    toIsomorphism (f , eqv) = f , toIso eqv
+
+module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
+  -- A wrapper around PathPrelude.≃
+  open Cubical.PathPrelude using (_≃_ ; isEquiv)
+  private
+    module _ {obverse : A → B} (e : isEquiv A B obverse) where
+      inverse : B → A
+      inverse b = fst (fst (e b))
+
+      reverse : B → A
+      reverse = inverse
+
+      areInverses : AreInverses obverse inverse
+      areInverses = record
+        { verso-recto = funExt verso-recto
+        ; recto-verso = funExt recto-verso
+        }
+        where
+        recto-verso : ∀ b → (obverse ∘ inverse) b ≡ b
+        recto-verso b = begin
+          (obverse ∘ inverse) b ≡⟨ sym (μ b) ⟩
+          b ∎
+          where
+          μ : (b : B) → b ≡ obverse (inverse b)
+          μ b = snd (fst (e b))
+        verso-recto : ∀ a → (inverse ∘ obverse) a ≡ a
+        verso-recto a = begin
+          (inverse ∘ obverse) a ≡⟨ sym h ⟩
+          a'                    ≡⟨ u' ⟩
+          a ∎
+          where
+          c : isContr (fiber obverse (obverse a))
+          c = e (obverse a)
+          fbr : fiber obverse (obverse a)
+          fbr = fst c
+          a' : A
+          a' = fst fbr
+          allC : (y : fiber obverse (obverse a)) → fbr ≡ y
+          allC = snd c
+          k : fbr ≡ (inverse (obverse a), _)
+          k = allC (inverse (obverse a) , sym (recto-verso (obverse a)))
+          h : a' ≡ inverse (obverse a)
+          h i = fst (k i)
+          u : fbr ≡ (a , refl)
+          u = allC (a , refl)
+          u' : a' ≡ a
+          u' i = fst (u i)
+
+      iso : Isomorphism obverse
+      iso = reverse , areInverses
+
+    toIsomorphism : {f : A → B} → isEquiv A B f → Isomorphism f
+    toIsomorphism = iso
+
+    ≃isEquiv : Equiv A B (isEquiv A B)
+    Equiv.fromIso     ≃isEquiv {f} (f~ , iso) = gradLemma f f~ rv vr
+      where
+      open AreInverses iso
+      rv : (b : B) → _ ≡ b
+      rv b i = recto-verso i b
+      vr : (a : A) → _ ≡ a
+      vr a i = verso-recto i a
+    Equiv.toIso        ≃isEquiv = toIsomorphism
+    Equiv.propIsEquiv  ≃isEquiv = P.propIsEquiv
+      where
+      import Cubical.NType.Properties as P
+
+  module Equiv≃ = Equiv ≃isEquiv
+
+module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
+  open Cubical.PathPrelude using (_≃_)
+
+  -- Gives the quasi inverse from an equivalence.
+  module Equivalence (e : A ≃ B) where
+    open Equiv≃ A B public
+    private
+      iso : Isomorphism (fst e)
+      iso = snd (toIsomorphism e)
+
+    open AreInverses (snd iso) public
+
+module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
+  open import Cubical.PathPrelude renaming (_≃_ to _≃η_)
+  open import Cubical.Univalence using (_≃_)
+  module Equivalence′ (e : A ≃ B) where
+    private
+      doEta : A ≃ B → A ≃η B
+      doEta = {!!}
+
+      deEta : A ≃η B → A ≃ B
+      deEta = {!!}
+
+      e′ = doEta e
+
+      module E = Equivalence e′
+    open E hiding (toIsomorphism ; fromIsomorphism ; _~_) public
+
+  fromIsomorphism : A ≅ B → A ≃ B
+  fromIsomorphism (f , iso) = _≃_.con f (Equiv≃.fromIso _ _ iso)
+
+  toIsomorphism : A ≃ B → A ≅ B
+  toIsomorphism (_≃_.con f eqv) = f , Equiv≃.toIso _ _ eqv
+  -- private
+  --   module Equiv′ (e : A ≃ B) where
+  --     open _≃_ e renaming (eqv to obverse)
+
+  --     private
+  --       inverse : B → A
+  --       inverse b = fst (fst (isEqv b))
+
+  --     -- We can extract an isomorphism from an equivalence.
+  --     --
+  --     -- One way to do it would be to use univalence and coersion - but there's
+  --     -- probably a more straight-forward way that does not require breaking the
+  --     -- dependency graph between this module and Cubical.Univalence
+  --     areInverses : AreInverses obverse inverse
+  --     areInverses = record
+  --       { verso-recto = verso-recto
+  --       ; recto-verso = recto-verso
+  --       }
+  --       where
+  --       postulate
+  --         verso-recto : inverse ∘ obverse ≡ idFun A
+  --         recto-verso : obverse ∘ inverse ≡ idFun B
+
+  --     toIsomorphism : A ≅ B
+  --     toIsomorphism = obverse , (inverse , areInverses)
+
+  --     open AreInverses areInverses
+
+  --     equiv≃ : Equiv A B (isEquiv A B)
+  --     equiv≃ = {!!}
+
+  -- -- A wrapper around Univalence.≃
+  -- module Equiv≃′ = Equiv {!!}