From 35390c02d3852955ab3343c9740b3f089255fe2d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 12 Mar 2018 13:36:55 +0100 Subject: [PATCH] Stuff about univalence in the category of sets --- libs/cubical | 2 +- src/Cat/Categories/Sets.agda | 129 +++++++++++++++++++++++++---------- src/Cat/Category.agda | 69 ++++++++++++------- src/Cat/Category/Monad.agda | 4 +- src/Cat/Category/Yoneda.agda | 2 +- src/Cat/Wishlist.agda | 9 +-- 6 files changed, 146 insertions(+), 69 deletions(-) diff --git a/libs/cubical b/libs/cubical index a487c76..3a125a0 160000 --- a/libs/cubical +++ b/libs/cubical @@ -1 +1 @@ -Subproject commit a487c76a5f3ecf2752dabc9e5c3a8866fda28a19 +Subproject commit 3a125a0cb010903e6aa80569a0ca5339424eaf86 diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index c18b70a..a329a0f 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -4,10 +4,15 @@ module Cat.Categories.Sets where open import Agda.Primitive open import Data.Product -import Function +open import Function using (_∘_) -open import Cubical hiding (inverse ; _≃_ {- ; obverse ; recto-verso ; verso-recto -} ) -open import Cubical.Univalence using (_≃_ ; ua) +open import Cubical hiding (_≃_ ; inverse) +open import Cubical.Equivalence + renaming + ( _≅_ to _A≅_ ) + using + (_≃_ ; con ; AreInverses) +open import Cubical.Univalence open import Cubical.GradLemma open import Cat.Category @@ -27,7 +32,7 @@ module _ (ℓ : Level) where RawCategory.𝟙 SetsRaw = Function.id RawCategory._∘_ SetsRaw = Function._∘′_ - open RawCategory SetsRaw + open RawCategory SetsRaw hiding (_∘_) open Univalence SetsRaw isIdentity : IsIdentity Function.id @@ -62,48 +67,100 @@ module _ (ℓ : Level) where -- ordering should be swapped. areInverses : IsInverseOf {A = hA} {hB} obverse inverse areInverses = proj₂ (proj₂ iso) - verso-recto : ∀ a → (inverse Function.∘ obverse) a ≡ a + verso-recto : ∀ a → (inverse ∘ obverse) a ≡ a verso-recto a i = proj₁ areInverses i a recto-verso : ∀ b → (obverse Function.∘ inverse) b ≡ b recto-verso b i = proj₂ areInverses i b - univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) - univalent = gradLemma obverse inverse verso-recto recto-verso - where + private + univIso : (A ≡ B) A≅ (A ≃ B) + univIso = _≃_.toIsomorphism univalence + obverse' : A ≡ B → A ≃ B + obverse' = proj₁ univIso + inverse' : A ≃ B → A ≡ B + inverse' = proj₁ (proj₂ univIso) + -- Drop proof of being a set from both sides of an equality. + dropP : hA ≡ hB → A ≡ B + 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 eqv = proj₁ eqv , (proj₁ (proj₂ eqv)) , asPair + where + areeqv = proj₂ (proj₂ eqv) + asPair = + let module Inv = AreInverses areeqv + in Inv.verso-recto , Inv.recto-verso + obverse : hA ≡ hB → hA ≅ hB - obverse eq = {!res!} - where - -- Problem: How do I extract this equality from `eq`? - eqq : A ≡ B - eqq = {!!} - eq' : A ≃ B - eq' = fromEquality eqq - -- Problem: Why does this not satisfy the goal? - res : hA ≅ hB - res = toIsomorphism eq' + obverse = addE ∘ _≃_.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 eqv = obv , inv , asAreInverses + where + obv = proj₁ eqv + inv = proj₁ (proj₂ eqv) + areEq = proj₂ (proj₂ eqv) + asAreInverses : AreInverses A B 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 = {!!} + -- 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 inverse : hA ≅ hB → hA ≡ hB - inverse iso = res - where - eq : A ≡ B - eq = ua (fromIsomorphism iso) + inverse = addP ∘ inverse' ∘ isoToEquiv ∘ dropE - -- Use the fact that being an h-level level is a mere proposition. - -- This is almost provable using `Wishlist.isSetIsProp` - although - -- this creates homogenous paths. - isSetEq : (λ i → isSet (eq i)) [ isSetA ≡ isSetB ] - isSetEq = {!!} + -- open AreInverses (proj₂ (proj₂ univIso)) renaming + -- ( verso-recto to verso-recto' + -- ; recto-verso to recto-verso' + -- ) + -- 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)) + recto-verso' : obverse' ∘ inverse' ≡ Function.id + recto-verso' = AreInverses.recto-verso (proj₂ (proj₂ univIso)) + verso-recto : (iso : hA ≅ hB) → obverse (inverse iso) ≡ iso + verso-recto iso = begin + obverse (inverse iso) ≡⟨⟩ + ( addE ∘ _≃_.toIsomorphism + ∘ obverse' ∘ dropP ∘ addP + ∘ inverse' ∘ isoToEquiv + ∘ dropE) iso + ≡⟨⟩ + ( addE ∘ _≃_.toIsomorphism + ∘ obverse' + ∘ inverse' ∘ isoToEquiv + ∘ dropE) iso + ≡⟨ {!!} ⟩ -- obverse' inverse' are inverses + ( addE ∘ _≃_.toIsomorphism ∘ isoToEquiv ∘ dropE) iso + ≡⟨ {!!} ⟩ -- should be easy to prove + -- _≃_.toIsomorphism ∘ isoToEquiv ≡ id + (addE ∘ dropE) iso + ≡⟨⟩ + iso ∎ - res : hA ≡ hB - proj₁ (res i) = eq i - proj₂ (res i) = isSetEq i + -- Similar to above. + recto-verso : (eq : hA ≡ hB) → inverse (obverse eq) ≡ eq + recto-verso eq = begin + inverse (obverse eq) ≡⟨ {!!} ⟩ + eq ∎ - -- FIXME Either the name of inverse/obverse is flipped or - -- recto-verso/verso-recto is flipped. - recto-verso : ∀ y → (inverse Function.∘ obverse) y ≡ y - recto-verso x = {!!} - verso-recto : ∀ x → (obverse Function.∘ inverse) x ≡ x - verso-recto x = {!!} + -- Use the fact that being an h-level is a mere proposition. + -- This is almost provable using `Wishlist.isSetIsProp` - although + -- this creates homogenous paths. + isSetEq : (p : A ≡ B) → (λ i → isSet (p i)) [ isSetA ≡ isSetB ] + isSetEq = {!!} + + res : hA ≡ hB + proj₁ (res i) = {!!} + proj₂ (res i) = isSetEq {!!} i + univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) + univalent = {!gradLemma obverse inverse verso-recto recto-verso!} SetsIsCategory : IsCategory SetsRaw IsCategory.isAssociative SetsIsCategory = refl diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index e547a81..5a13f41 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -129,7 +129,9 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where Terminal : Set (ℓa ⊔ ℓb) Terminal = Σ Object IsTerminal --- Univalence is indexed by a raw category as well as an identity proof. +-- | Univalence is indexed by a raw category as well as an identity proof. +-- +-- FIXME Put this in `RawCategory` and index it on the witness to `isIdentity`. module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where open RawCategory ℂ module _ (isIdentity : IsIdentity 𝟙) where @@ -150,6 +152,8 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where -- iso-is-epi : Isomorphism f → Epimorphism {X = X} f -- iso-is-mono : Isomorphism f → Monomorphism {X = X} f -- +-- Sans `univalent` this would be what is referred to as a pre-category in +-- [HoTT]. record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where open RawCategory ℂ public open Univalence ℂ public @@ -248,51 +252,66 @@ module Propositionality {ℓa ℓb : Level} {C : RawCategory ℓa ℓb} where -- adverse effects this may have. isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ] isIdentity = propIsIdentity x X.isIdentity Y.isIdentity - done : x ≡ y U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ] → (b : Univalent a) → Set _ - U eqwal bbb = + U eqwal univ = (λ i → Univalent (eqwal i)) - [ X.univalent ≡ bbb ] + [ X.univalent ≡ univ ] P : (y : IsIdentity 𝟙) → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ y ] → Set _ - P y eq = ∀ (b' : Univalent y) → U eq b' - helper : ∀ (b' : Univalent X.isIdentity) + P y eq = ∀ (univ : Univalent y) → U eq univ + p : ∀ (b' : Univalent X.isIdentity) → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ] - helper univ = propUnivalent x X.univalent univ - foo = pathJ P helper Y.isIdentity isIdentity + p univ = propUnivalent x X.univalent univ + helper : P Y.isIdentity isIdentity + helper = pathJ P p Y.isIdentity isIdentity eqUni : U isIdentity Y.univalent - eqUni = foo Y.univalent - IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i - IC.isIdentity (done i) = isIdentity i + eqUni = helper Y.univalent + done : x ≡ y + IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i + IC.isIdentity (done i) = isIdentity i IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i - IC.univalent (done i) = eqUni i + IC.univalent (done i) = eqUni i propIsCategory : isProp (IsCategory C) propIsCategory = done -- | Univalent categories -- --- Just bundles up the data with witnesses inhabting the propositions. +-- Just bundles up the data with witnesses inhabiting the propositions. record Category (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where field - raw : RawCategory ℓa ℓb + raw : RawCategory ℓa ℓb {{isCategory}} : IsCategory raw open IsCategory isCategory public -Category≡ : {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} → Category.raw ℂ ≡ Category.raw 𝔻 → ℂ ≡ 𝔻 -Category≡ {ℂ = ℂ} {𝔻} eq i = record - { raw = eq i - ; isCategory = isCategoryEq i - } - where - open Category - module ℂ = Category ℂ - isCategoryEq : (λ i → IsCategory (eq i)) [ isCategory ℂ ≡ isCategory 𝔻 ] - isCategoryEq = {!!} +-- The fact that being a category is a mere proposition gives rise to this +-- equality principle for categories. +module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} where + private + module ℂ = Category ℂ + module 𝔻 = Category 𝔻 + + module _ (rawEq : ℂ.raw ≡ 𝔻.raw) where + private + P : (target : RawCategory ℓa ℓb) → ({!!} ≡ target) → Set _ + P _ eq = ∀ isCategory' → (λ i → IsCategory (eq i)) [ ℂ.isCategory ≡ isCategory' ] + + p : P ℂ.raw refl + p isCategory' = Propositionality.propIsCategory {!!} {!!} + + -- TODO Make and use heterogeneous version of Category≡ + isCategoryEq : (λ i → IsCategory (rawEq i)) [ ℂ.isCategory ≡ 𝔻.isCategory ] + isCategoryEq = {!!} + + Category≡ : ℂ ≡ 𝔻 + Category≡ i = record + { raw = rawEq i + ; isCategory = isCategoryEq i + } -- | Syntax for arrows- and composition in a given category. module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where @@ -318,7 +337,7 @@ module Opposite {ℓa ℓb : Level} where RawCategory._∘_ opRaw = Function.flip ℂ._∘_ open RawCategory opRaw - open Univalence opRaw + open Univalence opRaw isIdentity : IsIdentity 𝟙 isIdentity = swap ℂ.isIdentity diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index f020383..5a8d4c1 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -735,7 +735,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where m ∎ where lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id - lem = verso-recto Monoidal≃Kleisli + lem = {!!} -- verso-recto Monoidal≃Kleisli t : {ℓ : Level} {A B : Set ℓ} {a : _ → A} {b : B → _} → a ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ b ≡ a ∘ b t {a = a} {b} = cong (λ φ → a ∘ φ ∘ b) lem @@ -763,7 +763,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where ) m ≡⟨⟩ -- fromMonad and toMonad are inverses m ∎ where - t = cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli) + t = {!!} -- cong (λ φ → voe-2-3-1-fromMonad ∘ φ ∘ voe-2-3.voe-2-3-1.toMonad) (recto-verso Monoidal≃Kleisli) voe-isEquiv : isEquiv (voe-2-3-1 omap pure) (voe-2-3-2 omap pure) forth voe-isEquiv = gradLemma forth back forthEq backEq diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index 0e19c04..af7567a 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -29,7 +29,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where -- -- In stead we'll use an ad-hoc definition -- which is definitionally -- equivalent to that other one. - _⇑_ = CatExponential.prodObj + _⇑_ = CatExponential.object module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where fmap : Transformation (prshf A) (prshf B) diff --git a/src/Cat/Wishlist.agda b/src/Cat/Wishlist.agda index d23f52a..8a63dc4 100644 --- a/src/Cat/Wishlist.agda +++ b/src/Cat/Wishlist.agda @@ -4,12 +4,13 @@ open import Level open import Cubical.NType open import Data.Nat using (_≤_ ; z≤n ; s≤s) +open import Cubical.NType.Properties public using (propHasLevel) + postulate ntypeCommulative : ∀ {ℓ n m} {A : Set ℓ} → n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A module _ {ℓ : Level} {A : Set ℓ} where - -- This is §7.1.10 in [HoTT]. Andrea says the proof is in `cubical` but I - -- can't find it. - postulate propHasLevel : ∀ n → isProp (HasLevel n A) - isSetIsProp : isProp (isSet A) isSetIsProp = propHasLevel (S (S ⟨-2⟩)) + + propIsProp : isProp (isProp A) + propIsProp = propHasLevel (S ⟨-2⟩)