From 438978973da7b7c2cdec0a06d732c1fd20bd4240 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 15 Mar 2018 11:04:15 +0100 Subject: [PATCH] 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 | 44 +++---- src/Cat/Category.agda | 6 + src/Cat/Category/Monad/Voevodsky.agda | 19 +-- src/Cat/Equivalence.agda | 183 ++++++++++++++++++++++++++ 4 files changed, 212 insertions(+), 40 deletions(-) create mode 100644 src/Cat/Equivalence.agda diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index e395512..415b34e 100644 --- a/src/Cat/Categories/Sets.agda +++ b/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 - renaming - ( _≅_ to _A≅_ ) - using - (_≃_ ; con ; AreInverses) -open import Cubical.Univalence +open import Cubical.Univalence using (univalence ; con ; _≃_) 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 = _≃_.toIsomorphism univalence + univIso : (A ≡ B) Eqv.≅ (A ≃ B) + 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 A≅ B → A ≃ B - isoToEquiv = {!!} + isoToEquiv : A Eqv.≅ B → A ≃ B + isoToEquiv = Eeq.fromIsomorphism + -- 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 diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 5b2f025..5b84a79 100644 --- a/src/Cat/Category.agda +++ b/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. -- diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index 501068e..51cebec 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/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 - --- 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 +open import Cat.Equivalence 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 diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda new file mode 100644 index 0000000..8e1e92c --- /dev/null +++ b/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 {!!}