Provide composition of isEquiv's

src/Cat/Category.agda

@@ -189,24 +189,16 @@ record IsPreCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (ls
     iso→epi×mono iso = iso→epi iso , iso→mono iso
 
   propIsAssociative : isProp IsAssociative
-  propIsAssociative x y i = arrowsAreSets _ _ x y i
+  propIsAssociative = propPiImpl (λ _ → propPiImpl (λ _ → propPiImpl (λ _ → propPiImpl (λ _ → propPiImpl (λ _ → propPiImpl (λ _ → propPiImpl λ _ → arrowsAreSets _ _))))))
 
   propIsIdentity : ∀ {f : ∀ {A} → Arrow A A} → isProp (IsIdentity f)
-  propIsIdentity a b i
+  propIsIdentity = propPiImpl (λ _ → propPiImpl λ _ → propPiImpl (λ _ → propSig (arrowsAreSets _ _) λ _ → arrowsAreSets _ _))
-    = arrowsAreSets _ _ (fst a) (fst b) i
-    , arrowsAreSets _ _ (snd a) (snd b) i
 
   propArrowIsSet : isProp (∀ {A B} → isSet (Arrow A B))
-  propArrowIsSet a b i = isSetIsProp a b i
+  propArrowIsSet = propPiImpl λ _ → propPiImpl (λ _ → isSetIsProp)
 
   propIsInverseOf : ∀ {A B f g} → isProp (IsInverseOf {A} {B} f g)
-  propIsInverseOf x y = λ i →
+  propIsInverseOf = propSig (arrowsAreSets _ _) (λ _ → arrowsAreSets _ _)
-    let
-      h : fst x ≡ fst y
-      h = arrowsAreSets _ _ (fst x) (fst y)
-      hh : snd x ≡ snd y
-      hh = arrowsAreSets _ _ (snd x) (snd y)
-    in h i , hh i
 
   module _ {A B : Object} {f : Arrow A B} where
     isoIsProp : isProp (Isomorphism f)

src/Cat/Equivalence.agda

@@ -7,6 +7,8 @@ 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)
+
 module _ {ℓa ℓb : Level} where
   private
     ℓ = ℓa ⊔ ℓb
@@ -55,6 +57,50 @@ module _ {ℓ : Level} {A B : Set ℓ} {f : A → B}
     re-ve : f ∘ g ≡ idFun B
     re-ve = s (f ∘ g) (idFun B) (recto-verso x) (recto-verso y) i
 
+module _ {ℓ : Level} {A B : Set ℓ} (f : A → B)
+  (sA : isSet A) (sB : isSet B) where
+
+  propIsIso : isProp (Isomorphism f)
+  propIsIso = res
+        where
+        module _ (x y : Isomorphism f) where
+          module x = Σ x renaming (fst to inverse ; snd to areInverses)
+          module y = Σ y renaming (fst to inverse ; snd to areInverses)
+          module xA = AreInverses x.areInverses
+          module yA = AreInverses y.areInverses
+          -- I had a lot of difficulty using the corresponding proof where
+          -- AreInverses is defined. This is sadly a bit anti-modular. The
+          -- reason for my troubles is probably related to the type of objects
+          -- being hSet's rather than sets.
+          p : ∀ {f} g → isProp (AreInverses {A = A} {B} f g)
+          p {f} g xx yy i = record
+            { verso-recto = ve-re
+            ; recto-verso = re-ve
+            }
+            where
+            module xxA = AreInverses xx
+            module yyA = AreInverses yy
+            setPiB : ∀ {X : Set ℓ} → isSet (X → B)
+            setPiB = setPi (λ _ → sB)
+            setPiA : ∀ {X : Set ℓ} → isSet (X → A)
+            setPiA = setPi (λ _ → sA)
+            ve-re : g ∘ f ≡ idFun _
+            ve-re = setPiA _ _ xxA.verso-recto yyA.verso-recto i
+            re-ve : f ∘ g ≡ idFun _
+            re-ve = setPiB _ _ xxA.recto-verso yyA.recto-verso i
+          1eq : x.inverse ≡ y.inverse
+          1eq = begin
+            x.inverse                   ≡⟨⟩
+            x.inverse ∘ idFun _         ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym yA.recto-verso) ⟩
+            x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩
+            (x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) xA.verso-recto ⟩
+            idFun _ ∘ y.inverse         ≡⟨⟩
+            y.inverse                   ∎
+          2eq : (λ i → AreInverses f (1eq i)) [ x.areInverses ≡ y.areInverses ]
+          2eq = lemPropF p 1eq
+          res : x ≡ y
+          res i = 1eq i , 2eq i
+
 -- 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
@@ -132,7 +178,7 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where
 
 module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
   -- A wrapper around PathPrelude.≃
-  open Cubical.PathPrelude using (_≃_ ; isEquiv)
+  open Cubical.PathPrelude using (_≃_)
   private
     module _ {obverse : A → B} (e : isEquiv A B obverse) where
       inverse : B → A
@@ -202,6 +248,37 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where
 module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
   open Cubical.PathPrelude using (_≃_)
 
+  module _ {ℓc : Level} {C : Set ℓc} {f : A → B} {g : B → C} where
+
+    composeIsomorphism : Isomorphism f → Isomorphism g → Isomorphism (g ∘ f)
+    composeIsomorphism a b = f~ ∘ g~ , inv
+      where
+      open Σ a renaming (fst to f~ ; snd to inv-a)
+      module A = AreInverses inv-a
+      open Σ b renaming (fst to g~ ; snd to inv-b)
+      module B = AreInverses inv-b
+      inv : AreInverses (g ∘ f) (f~ ∘ g~)
+      inv = record
+        { verso-recto = begin
+          (f~ ∘ g~) ∘ (g ∘ f) ≡⟨⟩
+          f~ ∘ (g~ ∘ g) ∘ f   ≡⟨ cong (λ φ → f~ ∘ φ ∘ f) B.verso-recto ⟩
+          f~ ∘ idFun _ ∘ f    ≡⟨⟩
+          f~ ∘ f              ≡⟨ A.verso-recto ⟩
+          idFun A             ∎
+        ; recto-verso = begin
+          (g ∘ f) ∘ (f~ ∘ g~) ≡⟨⟩
+          g ∘ (f ∘ f~) ∘ g~   ≡⟨ cong (λ φ → g ∘ φ ∘ g~) A.recto-verso ⟩
+          g ∘ g~              ≡⟨ B.recto-verso ⟩
+          idFun C             ∎
+        }
+
+    composeIsEquiv : isEquiv A B f → isEquiv B C g → isEquiv A C (g ∘ f)
+    composeIsEquiv a b = Equiv≃.fromIso A C (composeIsomorphism a' b')
+      where
+      a' = Equiv≃.toIso A B a
+      b' = Equiv≃.toIso B C b
+
+
   -- Gives the quasi inverse from an equivalence.
   module Equivalence (e : A ≃ B) where
     open Equiv≃ A B public
@@ -212,31 +289,10 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
     open AreInverses (snd iso) public
 
     composeIso : {ℓc : Level} {C : Set ℓc} → (B ≅ C) → A ≅ C
-    composeIso {C = C} (g , g' , iso-g) = g ∘ obverse , inverse ∘ g' , inv
+    composeIso {C = C} (g , iso-g) = g ∘ obverse , composeIsomorphism iso iso-g
-      where
-      module iso-g = AreInverses iso-g
-      inv : AreInverses (g ∘ obverse) (inverse ∘ g')
-      AreInverses.verso-recto inv = begin
-        (inverse ∘ g') ∘ (g ∘ obverse)   ≡⟨⟩
-        (inverse ∘ (g' ∘ g) ∘ obverse)
-          ≡⟨ cong (λ φ → φ ∘ obverse) (cong (λ φ → inverse ∘ φ) iso-g.verso-recto) ⟩
-        (inverse ∘ idFun B ∘ obverse)    ≡⟨⟩
-        (inverse ∘ obverse)              ≡⟨ verso-recto ⟩
-        idFun A ∎
-      AreInverses.recto-verso inv = begin
-        g ∘ obverse ∘ inverse ∘ g'
-          ≡⟨ cong (λ φ → φ ∘ g') (cong (λ φ → g ∘ φ) recto-verso) ⟩
-        g ∘ idFun B ∘ g' ≡⟨⟩
-        g ∘ g'           ≡⟨ iso-g.recto-verso ⟩
-        idFun C ∎
 
     compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C
-    compose {C = C} e = A≃C.fromIsomorphism is
+    compose (f , isEquiv) = f ∘ obverse , composeIsEquiv (snd e) isEquiv
-      where
-      module B≃C = Equiv≃ B C
-      module A≃C = Equiv≃ A C
-      is : A ≅ C
-      is = composeIso (B≃C.toIsomorphism e)
 
     symmetryIso : B ≅ A
     symmetryIso
@@ -288,3 +344,111 @@ module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
 
   toIsomorphism : A ≃ B → A ≅ B
   toIsomorphism (_≃_.con f eqv) = f , Equiv≃.toIso _ _ eqv
+
+-- A few results that I have not generalized to work with both the eta and no-eta variable of ≃
+module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where
+  open NoEta
+  open import Cubical.Univalence using (_≃_)
+
+  -- Equality on sigma's whose second component is a proposition is equivalent
+  -- to equality on their first components.
+  equivPropSig : ((x : A) → isProp (P x)) → (p q : Σ A P)
+    → (p ≡ q) ≃ (fst p ≡ fst q)
+  equivPropSig pA p q = fromIsomorphism iso
+    where
+    f : ∀ {p q} → p ≡ q → fst p ≡ fst q
+    f e i = fst (e i)
+    g : ∀ {p q} → fst p ≡ fst q → p ≡ q
+    g {p} {q} = lemSig pA p q
+    ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e
+    ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e)
+              (\ i j → p .fst , propSet (pA (p .fst)) (p .snd) (p .snd) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .snd) (λ i → p .snd) i j ) q
+    re-ve : (e : fst p ≡ fst q) → (f {p} {q} ∘ g {p} {q}) e ≡ e
+    re-ve e = refl
+    inv : AreInverses (f {p} {q}) (g {p} {q})
+    inv = record
+      { verso-recto = funExt ve-re
+      ; recto-verso = funExt re-ve
+      }
+    iso : (p ≡ q) ≅ (fst p ≡ fst q)
+    iso = f , g , inv
+
+  -- Sigma that are equivalent on all points in the second projection are
+  -- equivalent.
+  equivSigSnd : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)}
+    → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q
+  equivSigSnd {Q = Q} eA = res
+    where
+    f : Σ A P → Σ A Q
+    f (a , pA) = a , _≃_.eqv (eA a) pA
+    g : Σ A Q → Σ A P
+    g (a , qA) = a , g' qA
+      where
+      k : Isomorphism _
+      k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+      open Σ k renaming (fst to g')
+    ve-re : (x : Σ A P) → (g ∘ f) x ≡ x
+    ve-re x i = fst x , eq i
+      where
+      eq : snd ((g ∘ f) x) ≡ snd x
+      eq = begin
+        snd ((g ∘ f) x) ≡⟨⟩
+        snd (g (f (a , pA))) ≡⟨⟩
+        g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩
+        pA ∎
+        where
+        open Σ x renaming (fst to a ; snd to pA)
+        k : Isomorphism _
+        k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+        open Σ k renaming (fst to g' ; snd to inv)
+        module A = AreInverses inv
+        -- anti-funExt
+        lem : (g' ∘ (_≃_.eqv (eA a))) pA ≡ pA
+        lem i = A.verso-recto i pA
+    re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x
+    re-ve x i = fst x , eq i
+      where
+      open Σ x renaming (fst to a ; snd to qA)
+      eq = begin
+        snd ((f ∘ g) x)                 ≡⟨⟩
+        _≃_.eqv (eA a) (g' qA)            ≡⟨ (λ i → A.recto-verso i qA) ⟩
+        qA                                ∎
+        where
+        k : Isomorphism _
+        k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a))
+        open Σ k renaming (fst to g' ; snd to inv)
+        module A = AreInverses inv
+    inv : AreInverses f g
+    inv = record
+      { verso-recto = funExt ve-re
+      ; recto-verso = funExt re-ve
+      }
+    iso : Σ A P ≅ Σ A Q
+    iso = f , g , inv
+    res : Σ A P ≃ Σ A Q
+    res = fromIsomorphism iso
+
+module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where
+  open NoEta
+  open import Cubical.Univalence using (_≃_)
+  -- Equivalence is equivalent to isomorphism when the domain and codomain of
+  -- the equivalence is a set.
+  equivSetIso : isSet A → isSet B → (f : A → B)
+    → isEquiv A B f ≃ Isomorphism f
+  equivSetIso sA sB f =
+    let
+      obv : isEquiv A B f → Isomorphism f
+      obv = Equiv≃.toIso A B
+      inv : Isomorphism f → isEquiv A B f
+      inv = Equiv≃.fromIso A B
+      re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x
+      re-ve = Equiv≃.inverse-from-to-iso A B
+      ve-re : (x : Isomorphism f)       → (obv ∘ inv) x ≡ x
+      ve-re = Equiv≃.inverse-to-from-iso A B sA sB
+      iso : isEquiv A B f ≅ Isomorphism f
+      iso = obv , inv ,
+        record
+          { verso-recto = funExt re-ve
+          ; recto-verso = funExt ve-re
+          }
+    in fromIsomorphism iso

src/Cat/Prelude.agda

@@ -23,7 +23,8 @@ open import Cubical.NType
 open import Cubical.NType.Properties
   using
     ( lemPropF ; lemSig ;  lemSigP ; isSetIsProp
-    ; propPi ; propHasLevel ; setPi ; propSet)
+    ; propPi ; propPiImpl ; propHasLevel ; setPi ; propSet
+    ; propSig)
   public
 
 propIsContr : {ℓ : Level} → {A : Set ℓ} → isProp (isContr A)