From bbe94606479123f66bd44ee0c014e9e0aaba8df1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 5 Apr 2018 20:41:14 +0200 Subject: [PATCH] Provide composition of isEquiv's --- src/Cat/Category.agda | 16 +-- src/Cat/Equivalence.agda | 212 ++++++++++++++++++++++++++++++++++----- src/Cat/Prelude.agda | 3 +- 3 files changed, 194 insertions(+), 37 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 135e1a7..09ac382 100644 --- a/src/Cat/Category.agda +++ b/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 - = arrowsAreSets _ _ (fst a) (fst b) i - , arrowsAreSets _ _ (snd a) (snd b) i + propIsIdentity = propPiImpl (λ _ → propPiImpl λ _ → propPiImpl (λ _ → propSig (arrowsAreSets _ _) λ _ → arrowsAreSets _ _)) 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 → - 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 + propIsInverseOf = propSig (arrowsAreSets _ _) (λ _ → arrowsAreSets _ _) module _ {A B : Object} {f : Arrow A B} where isoIsProp : isProp (Isomorphism f) diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index b63e4ec..7d976af 100644 --- a/src/Cat/Equivalence.agda +++ b/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 - 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 ∎ + composeIso {C = C} (g , iso-g) = g ∘ obverse , composeIsomorphism iso iso-g compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C - compose {C = C} e = A≃C.fromIsomorphism is - where - module B≃C = Equiv≃ B C - module A≃C = Equiv≃ A C - is : A ≅ C - is = composeIso (B≃C.toIsomorphism e) + compose (f , isEquiv) = f ∘ obverse , composeIsEquiv (snd e) isEquiv 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 diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index 7a239d5..e18cb72 100644 --- a/src/Cat/Prelude.agda +++ b/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)