From 7065455712c37fe0c91b3c66fb59c835835047ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 13 Mar 2018 11:29:13 +0100 Subject: [PATCH 01/38] More readable goal for voevodsky's construction --- BACKLOG.md | 14 +++++++---- src/Cat/Category/Monad/Voevodsky.agda | 35 ++++++++++++++++++++------- 2 files changed, 35 insertions(+), 14 deletions(-) diff --git a/BACKLOG.md b/BACKLOG.md index ed1b205..c8fb54b 100644 --- a/BACKLOG.md +++ b/BACKLOG.md @@ -1,13 +1,14 @@ Backlog ======= -Prove postulates in `Cat.Wishlist` -`ntypeCommulative` might be there as well. - -Prove that the opposite category is a category. +Prove postulates in `Cat.Wishlist`: + * `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A` Prove univalence for the category of + * the opposite category * sets + This does not follow trivially from `Cubical.Univalence.univalence` because + objects are not `Set` but `hSet` * functors and natural transformations Prove: @@ -24,7 +25,10 @@ Prove: * Monad * Monoidal monad ✓ * Kleisli monad ✓ - * Problem 2.3 in voe + * Kleisli ≃ Monoidal ✓ + * Problem 2.3 in [voe] * 1st contruction ~ monoidal ✓ * 2nd contruction ~ klesli ✓ * 1st ≃ 2nd ✗ + I've managed to set this up so I should be able to reuse the proof that + Kleisli ≃ Monoidal, but I don't know why it doesn't typecheck. diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index 3a807de..f794b31 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -7,6 +7,7 @@ module Cat.Category.Monad.Voevodsky where open import Agda.Primitive open import Data.Product +open import Function using (_∘_ ; _$_) open import Cubical open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) @@ -20,13 +21,26 @@ import Cat.Category.Monad.Monoidal as Monoidal import Cat.Category.Monad.Kleisli as Kleisli open import Cat.Categories.Fun +-- Utilities +module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where + module _ (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 ℓ = ℓa ⊔ ℓb module ℂ = Category ℂ open ℂ using (Object ; Arrow) open NaturalTransformation ℂ ℂ - open import Function using (_∘_ ; _$_) module M = Monoidal ℂ module K = Kleisli ℂ @@ -162,7 +176,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ∘ Monoidal→Kleisli ∘ Kleisli→Monoidal ∘ §2-3.§2.toMonad - ) m ≡⟨ u ⟩ + ) m ≡⟨ cong (λ φ → φ m) t ⟩ -- Monoidal→Kleisli and Kleisli→Monoidal are inverses -- I should be able to prove this using congruence and `lem` below. ( §2-fromMonad @@ -173,14 +187,12 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ) m ≡⟨⟩ -- fromMonad and toMonad are inverses m ∎ where - lem : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id - lem = {!!} -- verso-recto Monoidal≃Kleisli + ve-re : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id + ve-re = recto-verso Monoidal≃Kleisli t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) ≡ (§2-fromMonad ∘ §2-3.§2.toMonad) - t = cong (λ φ → §2-fromMonad ∘ (λ{ {ω} → φ {{!????!}}}) ∘ §2-3.§2.toMonad) {!lem!} - u : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) m - ≡ (§2-fromMonad ∘ §2-3.§2.toMonad) m - u = cong (λ φ → φ m) t + -- Why can I not give φ in the first hole like I do below in `backEq.t`? + t = cong (λ φ → §2-fromMonad ∘ {!φ!} ∘ §2-3.§2.toMonad) ve-re backEq : ∀ m → (back ∘ forth) m ≡ m backEq m = begin @@ -202,7 +214,12 @@ module voe {ℓ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) + re-ve : Kleisli→Monoidal ∘ Monoidal→Kleisli ≡ Function.id + re-ve = verso-recto Monoidal≃Kleisli + t : §1-fromMonad ∘ Kleisli→Monoidal ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad + ≡ §1-fromMonad ∘ §2-3.§1.toMonad + -- Why does `re-ve` not satisfy this goal? + t = cong (λ φ → §1-fromMonad ∘ φ ∘ §2-3.§1.toMonad) ({!re-ve!}) voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth voe-isEquiv = gradLemma forth back forthEq backEq From 091e77b583d37716f51aca8d98dc2d636bf9d964 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 14 Mar 2018 10:23:23 +0100 Subject: [PATCH 02/38] Rename IsProduct.isProduct to IsProduct.ump [WIP]: Also some stuff about propositionality for products. --- src/Cat/Categories/Cat.agda | 2 +- src/Cat/Categories/Sets.agda | 2 +- src/Cat/Category/Product.agda | 69 +++++++++++++++++++++++++++++++---- 3 files changed, 64 insertions(+), 9 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 8c7bcbb..f013c82 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -167,7 +167,7 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where RawProduct.proj₂ rawProduct = P.proj₂ isProduct : IsProduct Catℓ _ _ rawProduct - IsProduct.isProduct isProduct = P.isProduct + IsProduct.ump isProduct = P.isProduct product : Product Catℓ ℂ 𝔻 Product.raw product = rawProduct diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index a329a0f..e395512 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -208,7 +208,7 @@ module _ {ℓ : Level} where RawProduct.proj₂ rawProduct = Data.Product.proj₂ isProduct : IsProduct 𝓢 _ _ rawProduct - IsProduct.isProduct isProduct {X = X} f g + IsProduct.ump isProduct {X = X} f g = (f &&& g) , lem {0X = X} f g product : Product 𝓢 0A 0B diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index dff488a..1ddeed9 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -3,6 +3,8 @@ module Cat.Category.Product where open import Agda.Primitive open import Cubical +open import Cubical.NType.Properties using (lemPropF) + open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂) open import Cat.Category hiding (module Propositionality) @@ -24,13 +26,13 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where record IsProduct (raw : RawProduct) : Set (ℓa ⊔ ℓb) where open RawProduct raw public field - isProduct : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) + ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) → ∃![ f×g ] (ℂ [ proj₁ ∘ f×g ] ≡ f P.× ℂ [ proj₂ ∘ f×g ] ≡ g) -- | Arrow product _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ]) → ℂ [ X , object ] - _P[_×_] π₁ π₂ = P.proj₁ (isProduct π₁ π₂) + _P[_×_] π₁ π₂ = P.proj₁ (ump π₁ π₂) record Product : Set (ℓa ⊔ ℓb) where field @@ -59,10 +61,63 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where × ℂ [ g ∘ snd ] ] -module Propositionality {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where - -- TODO I'm not sure this is actually provable. Check with Thierry. - propProduct : isProp (Product ℂ A B) - propProduct = {!!} +module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where + private + open Category ℂ + module _ (raw : RawProduct ℂ A B) where + module _ (x y : IsProduct ℂ A B raw) where + private + module x = IsProduct x + module y = IsProduct y + + module _ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) where + prodAux : x.ump f g ≡ y.ump f g + prodAux = {!!} + + propIsProduct' : x ≡ y + propIsProduct' i = record { ump = λ f g → prodAux f g i } + + propIsProduct : isProp (IsProduct ℂ A B raw) + propIsProduct = propIsProduct' + + Product≡ : {x y : Product ℂ A B} → (Product.raw x ≡ Product.raw y) → x ≡ y + Product≡ {x} {y} p i = record { raw = p i ; isProduct = q i } + where + q : (λ i → IsProduct ℂ A B (p i)) [ Product.isProduct x ≡ Product.isProduct y ] + q = lemPropF propIsProduct p + +module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where + open Category ℂ + private + module _ (x y : HasProducts ℂ) where + private + module x = HasProducts x + module y = HasProducts y + module _ (A B : Object) where + module pX = Product (x.product A B) + module pY = Product (y.product A B) + objEq : pX.object ≡ pY.object + objEq = {!!} + proj₁Eq : (λ i → ℂ [ objEq i , A ]) [ pX.proj₁ ≡ pY.proj₁ ] + proj₁Eq = {!!} + proj₂Eq : (λ i → ℂ [ objEq i , B ]) [ pX.proj₂ ≡ pY.proj₂ ] + proj₂Eq = {!!} + rawEq : pX.raw ≡ pY.raw + RawProduct.object (rawEq i) = objEq i + RawProduct.proj₁ (rawEq i) = {!!} + RawProduct.proj₂ (rawEq i) = {!!} + + isEq : (λ i → IsProduct ℂ A B (rawEq i)) [ pX.isProduct ≡ pY.isProduct ] + isEq = {!!} + + appEq : x.product A B ≡ y.product A B + appEq = Product≡ rawEq + + productEq : x.product ≡ y.product + productEq i = λ A B → appEq A B i + + propHasProducts' : x ≡ y + propHasProducts' i = record { product = productEq i } propHasProducts : isProp (HasProducts ℂ) - propHasProducts = {!!} + propHasProducts = propHasProducts' From 7aec22b30af72dd645298b6134af0579cc9c2702 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 14 Mar 2018 11:00:52 +0100 Subject: [PATCH 03/38] Expose both monad formulations qualified from Cat.Category.Monad --- src/Cat/Category/Monad.agda | 7 +++++-- src/Cat/Category/Monad/Voevodsky.agda | 4 +--- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 2f42f32..7f8637a 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -31,10 +31,13 @@ open import Cubical.GradLemma using (gradLemma) open import Cat.Category open import Cat.Category.Functor as F open import Cat.Category.NaturalTransformation -open import Cat.Category.Monad.Monoidal as Monoidal public -open import Cat.Category.Monad.Kleisli as Kleisli +import Cat.Category.Monad.Monoidal +import Cat.Category.Monad.Kleisli open import Cat.Categories.Fun +module Monoidal = Cat.Category.Monad.Monoidal +module Kleisli = Cat.Category.Monad.Kleisli + -- | The monoidal- and kleisli presentation of monads are equivalent. module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where private diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index d64d3f7..4409039 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -16,9 +16,7 @@ open import Cubical.GradLemma using (gradLemma) open import Cat.Category open import Cat.Category.Functor as F open import Cat.Category.NaturalTransformation -open import Cat.Category.Monad using (Monoidal≃Kleisli) -import Cat.Category.Monad.Monoidal as Monoidal -import Cat.Category.Monad.Kleisli as Kleisli +open import Cat.Category.Monad open import Cat.Categories.Fun -- Utilities From 360e2b95dd6fc8772dfdbb31ac6b0ba5a1ba8592 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 14 Mar 2018 11:20:07 +0100 Subject: [PATCH 04/38] Make parameter to monad equivalence explicit --- src/Cat/Category/Monad.agda | 2 +- src/Cat/Category/Monad/Voevodsky.agda | 26 +++++++++++++++++--------- 2 files changed, 18 insertions(+), 10 deletions(-) diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 7f8637a..d741ccd 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -39,7 +39,7 @@ module Monoidal = Cat.Category.Monad.Monoidal module Kleisli = Cat.Category.Monad.Kleisli -- | The monoidal- and kleisli presentation of monads are equivalent. -module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} where +module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where private module ℂ = Category ℂ open ℂ using (Object ; Arrow ; 𝟙 ; _∘_ ; _>>>_) diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index 4409039..501068e 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -21,7 +21,7 @@ open import Cat.Categories.Fun -- Utilities module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where - module _ (e : A ≃ B) where + module Equivalence (e : A ≃ B) where obverse : A → B obverse = proj₁ e @@ -145,13 +145,25 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ; isMnd = K.Monad.isMonad m } + -- | In the following we seek to transform the equivalence `Monoidal≃Kleisli` + -- | 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 - Monoidal→Kleisli = proj₁ Monoidal≃Kleisli + Monoidal→Kleisli = E.obverse Kleisli→Monoidal : K.Monad → M.Monad - Kleisli→Monoidal = inverse Monoidal≃Kleisli + Kleisli→Monoidal = E.reverse + + ve-re : Kleisli→Monoidal ∘ Monoidal→Kleisli ≡ Function.id + ve-re = E.verso-recto + + re-ve : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id + re-ve = E.recto-verso forth : §2-3.§1 omap pure → §2-3.§2 omap pure forth = §2-fromMonad ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad @@ -185,11 +197,9 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ) m ≡⟨⟩ -- fromMonad and toMonad are inverses m ∎ where - ve-re : Monoidal→Kleisli ∘ Kleisli→Monoidal ≡ Function.id - ve-re = {!recto-verso Monoidal≃Kleisli!} t' : ((Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure}) ≡ §2-3.§2.toMonad - t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) ve-re + t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) {!re-ve!} cong-d : ∀ {ℓ} {A : Set ℓ} {ℓ'} {B : A → Set ℓ'} {x y : A} → (f : (x : A) → B x) → (eq : x ≡ y) → PathP (\ i → B (eq i)) (f x) (f y) cong-d f p = λ i → f (p i) @@ -226,12 +236,10 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ) m ≡⟨⟩ -- fromMonad and toMonad are inverses m ∎ where - re-ve : Kleisli→Monoidal ∘ Monoidal→Kleisli ≡ Function.id - re-ve = verso-recto Monoidal≃Kleisli t : §1-fromMonad ∘ Kleisli→Monoidal ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad ≡ §1-fromMonad ∘ §2-3.§1.toMonad -- Why does `re-ve` not satisfy this goal? - t = cong (λ φ → §1-fromMonad ∘ φ ∘ §2-3.§1.toMonad) ({!re-ve!}) + t = cong (λ φ → §1-fromMonad ∘ φ ∘ §2-3.§1.toMonad) ({!ve-re!}) voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth voe-isEquiv = gradLemma forth back forthEq backEq 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 05/38] 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 {!!} From f7f8953a429aec43cd00382aeb5b8c562f1ef4c6 Mon Sep 17 00:00:00 2001 From: Andrea Vezzosi Date: Thu, 15 Mar 2018 13:39:42 +0000 Subject: [PATCH 06/38] Voe: Use the isomorphism directly for better computation --- src/Cat/Category/Monad.agda | 5 +++++ src/Cat/Category/Monad/Voevodsky.agda | 14 ++++---------- 2 files changed, 9 insertions(+), 10 deletions(-) diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index d741ccd..3eef523 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -210,5 +210,10 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where eqv : isEquiv M.Monad K.Monad forth eqv = gradLemma forth back fortheq backeq + open import Cat.Equivalence + + Monoidal≅Kleisli : M.Monad ≅ K.Monad + Monoidal≅Kleisli = forth , (back , (record { verso-recto = funExt backeq ; recto-verso = funExt fortheq })) + Monoidal≃Kleisli : M.Monad ≃ K.Monad Monoidal≃Kleisli = forth , eqv diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index 51cebec..5f27ed0 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -136,7 +136,7 @@ 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 - module E = Equivalence (Monoidal≃Kleisli ℂ) + module E = AreInverses (Monoidal≅Kleisli ℂ .proj₂ .proj₂) Monoidal→Kleisli : M.Monad → K.Monad Monoidal→Kleisli = E.obverse @@ -184,22 +184,16 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where where t' : ((Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure}) ≡ §2-3.§2.toMonad - t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) {!re-ve!} cong-d : ∀ {ℓ} {A : Set ℓ} {ℓ'} {B : A → Set ℓ'} {x y : A} → (f : (x : A) → B x) → (eq : x ≡ y) → PathP (\ i → B (eq i)) (f x) (f y) cong-d f p = λ i → f (p i) + t' = cong (\ φ → φ ∘ §2-3.§2.toMonad) re-ve t : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad {omap} {pure}) ≡ (§2-fromMonad ∘ §2-3.§2.toMonad) t = cong-d (\ f → §2-fromMonad ∘ f) t' u : (§2-fromMonad ∘ (Monoidal→Kleisli ∘ Kleisli→Monoidal) ∘ §2-3.§2.toMonad) m ≡ (§2-fromMonad ∘ §2-3.§2.toMonad) m - u = cong (\ f → f m) t -{- -(K.RawMonad.omap (K.Monad.raw (?0 ℂ omap pure m i (§2-3.§2.toMonad m))) x) - = (omap x) : Object -(K.RawMonad.pure (K.Monad.raw (?0 ℂ omap pure m x (§2-3.§2.toMonad x)))) - = pure : Arrow X (_350 ℂ omap pure m x x X) --} + u = cong (\ φ → φ m) t backEq : ∀ m → (back ∘ forth) m ≡ m backEq m = begin @@ -224,7 +218,7 @@ module voe {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where t : §1-fromMonad ∘ Kleisli→Monoidal ∘ Monoidal→Kleisli ∘ §2-3.§1.toMonad ≡ §1-fromMonad ∘ §2-3.§1.toMonad -- Why does `re-ve` not satisfy this goal? - t = cong (λ φ → §1-fromMonad ∘ φ ∘ §2-3.§1.toMonad) ({!ve-re!}) + t i m = §1-fromMonad (ve-re i (§2-3.§1.toMonad m)) voe-isEquiv : isEquiv (§2-3.§1 omap pure) (§2-3.§2 omap pure) forth voe-isEquiv = gradLemma forth back forthEq backEq From f69ab0ee62c500508dc8c9f936f8cd623c52c9ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 19 Mar 2018 14:08:59 +0100 Subject: [PATCH 07/38] [WIP] Univalence for the category of hSets --- Makefile | 3 + src/Cat/Categories/Sets.agda | 210 +++++++++++++++-------------------- src/Cat/Equivalence.agda | 69 +++++------- 3 files changed, 120 insertions(+), 162 deletions(-) diff --git a/Makefile b/Makefile index 051f9ce..f2e26be 100644 --- a/Makefile +++ b/Makefile @@ -1,2 +1,5 @@ build: src/**.agda agda src/Cat.agda + +clean: + rm src/**/*.agdai diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 415b34e..5de99e3 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -6,18 +6,22 @@ open import Agda.Primitive open import Data.Product open import Function using (_∘_) -open import Cubical hiding (_≃_ ; inverse) -open import Cubical.Univalence using (univalence ; con ; _≃_) +-- open import Cubical using (funExt ; refl ; isSet ; isProp ; _≡_ ; isEquiv ; sym ; trans ; _[_≡_] ; I ; Path ; PathP) +open import Cubical hiding (_≃_) +open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv) 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) +open import Cat.Equivalence as Eqv renaming (module NoEta to Eeq) using (AreInverses) -module Equivalence = NoEta.Equivalence′ -module Eeq = NoEta +module Equivalence = Eeq.Equivalence′ +postulate + _⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C + sym≃ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A ≃ B → B ≃ A +infixl 10 _⊙_ module _ (ℓ : Level) where private @@ -25,7 +29,7 @@ module _ (ℓ : Level) where open import Cubical.Universe SetsRaw : RawCategory (lsuc ℓ) ℓ - RawCategory.Object SetsRaw = hSet + RawCategory.Object SetsRaw = hSet {ℓ} RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U RawCategory.𝟙 SetsRaw = Function.id RawCategory._∘_ SetsRaw = Function._∘′_ @@ -40,125 +44,95 @@ module _ (ℓ : Level) where arrowsAreSets : ArrowsAreSets arrowsAreSets {B = (_ , s)} = setPi λ _ → s + isIso = Eqv.Isomorphism + module _ {hA hB : hSet {ℓ}} where + open Σ hA renaming (proj₁ to A ; proj₂ to sA) + open Σ hB renaming (proj₁ to B ; proj₂ to sB) + lem1 : (f : A → B) → isSet A → isSet B → isProp (isIso f) + lem1 f sA sB = res + where + module _ (x y : isIso f) where + module x = Σ x renaming (proj₁ to inverse ; proj₂ to areInverses) + module y = Σ y renaming (proj₁ to inverse ; proj₂ 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 + ve-re : g ∘ f ≡ Function.id + ve-re = arrowsAreSets {A = hA} {B = hA} _ _ xxA.verso-recto yyA.verso-recto i + re-ve : f ∘ g ≡ Function.id + re-ve = arrowsAreSets {A = hB} {B = hB} _ _ xxA.recto-verso yyA.recto-verso i + 1eq : x.inverse ≡ y.inverse + 1eq = begin + x.inverse ≡⟨⟩ + x.inverse ∘ Function.id ≡⟨ cong (λ φ → x.inverse ∘ φ) (sym yA.recto-verso) ⟩ + x.inverse ∘ (f ∘ y.inverse) ≡⟨⟩ + (x.inverse ∘ f) ∘ y.inverse ≡⟨ cong (λ φ → φ ∘ y.inverse) xA.verso-recto ⟩ + Function.id ∘ 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 + module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where + postulate + lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P) + → (p ≡ q) ≃ (proj₁ p ≡ proj₁ q) + lem3 : {Q : A → Set ℓb} → ((x : A) → P x ≃ Q x) + → Σ A P ≃ Σ A Q + + module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where + postulate + lem4 : isSet A → isSet B → (f : A → B) + → isEquiv A B f ≃ isIso f + module _ {hA hB : Object} where private A = proj₁ hA - isSetA : isSet A - isSetA = proj₂ hA + sA = proj₂ hA B = proj₁ hB - isSetB : isSet B - isSetB = proj₂ hB + sB = proj₂ hB - toIsomorphism : A ≃ B → hA ≅ hB - toIsomorphism e = obverse , inverse , verso-recto , recto-verso + postulate + -- lem3 and the equivalence from lem4 + step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) + -- univalence + step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) + -- lem2 with propIsSet + step2 : (A ≡ B) ≃ (hA ≡ hB) + -- Go from an isomorphism on sets to an isomorphism on homotopic sets + trivial? : (hA ≅ hB) ≃ Σ (A → B) isIso + trivial? = sym≃ (Eeq.fromIsomorphism res) + where + fwd : Σ (A → B) isIso → hA ≅ hB + fwd (f , g , inv) = f , g , inv.toPair where - open Equivalence e - - fromIsomorphism : hA ≅ hB → A ≃ B - fromIsomorphism iso = con obverse (gradLemma obverse inverse recto-verso verso-recto) - where - obverse : A → B - obverse = proj₁ iso - inverse : B → A - inverse = proj₁ (proj₂ iso) - -- FIXME IsInverseOf should change name to AreInverses and the - -- ordering should be swapped. - areInverses : IsInverseOf {A = hA} {hB} obverse inverse - areInverses = proj₂ (proj₂ iso) - 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 - - private - univIso : (A ≡ B) Eqv.≅ (A ≃ B) - univIso = Eeq.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 Eqv.≅ B → hA ≅ hB - addE eqv = proj₁ eqv , (proj₁ (proj₂ eqv)) , asPair - where - areeqv = proj₂ (proj₂ eqv) - asPair = - let module Inv = Eqv.AreInverses areeqv - in Inv.verso-recto , Inv.recto-verso - - obverse : hA ≡ hB → hA ≅ hB - 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 Eqv.≅ B - dropE eqv = obv , inv , asAreInverses - where - obv = proj₁ eqv - inv = proj₁ (proj₂ eqv) - areEq = proj₂ (proj₂ eqv) - asAreInverses : Eqv.AreInverses obv inv - asAreInverses = record { verso-recto = proj₁ areEq ; recto-verso = proj₂ areEq } - - 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 - inverse : hA ≅ hB → hA ≡ hB - inverse = addP ∘ inverse' ∘ isoToEquiv ∘ dropE - - -- 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' = Eqv.AreInverses.verso-recto (proj₂ (proj₂ univIso)) - recto-verso' : obverse' ∘ inverse' ≡ Function.id - 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 ∘ Eeq.toIsomorphism - ∘ obverse' ∘ dropP ∘ addP - ∘ inverse' ∘ isoToEquiv - ∘ dropE) iso - ≡⟨⟩ - ( addE ∘ Eeq.toIsomorphism - ∘ obverse' - ∘ inverse' ∘ isoToEquiv - ∘ dropE) iso - ≡⟨ {!!} ⟩ -- obverse' inverse' are inverses - ( addE ∘ Eeq.toIsomorphism ∘ isoToEquiv ∘ dropE) iso - ≡⟨ {!!} ⟩ -- should be easy to prove - -- _≃_.toIsomorphism ∘ isoToEquiv ≡ id - (addE ∘ dropE) iso - ≡⟨⟩ - iso ∎ - - -- Similar to above. - recto-verso : (eq : hA ≡ hB) → inverse (obverse eq) ≡ eq - recto-verso eq = begin - inverse (obverse eq) ≡⟨ {!!} ⟩ - eq ∎ - - -- 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 + module inv = AreInverses inv + bwd : hA ≅ hB → Σ (A → B) isIso + bwd (f , g , x , y) = f , g , record { verso-recto = x ; recto-verso = y } + res : Σ (A → B) isIso Eqv.≅ (hA ≅ hB) + res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl } + conclusion : (hA ≅ hB) ≃ (hA ≡ hB) + conclusion = trivial? ⊙ step0 ⊙ step1 ⊙ step2 + t : (hA ≡ hB) ≃ (hA ≅ hB) + t = sym≃ conclusion + -- TODO Is the morphism `(_≃_.eqv conclusion)` the same as + -- `(id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)` ? + res : isEquiv (hA ≡ hB) (hA ≅ hB) (_≃_.eqv t) + res = _≃_.isEqv t + module _ {hA hB : hSet {ℓ}} where univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) - univalent = {!gradLemma obverse inverse verso-recto recto-verso!} + univalent = let k = _≃_.isEqv (sym≃ conclusion) in {!!} SetsIsCategory : IsCategory SetsRaw IsCategory.isAssociative SetsIsCategory = refl diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index 8e1e92c..62df900 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -21,6 +21,8 @@ module _ {ℓa ℓb : Level} where obverse = f reverse = g inverse = reverse + toPair : Σ _ _ + toPair = verso-recto , recto-verso Isomorphism : (f : A → B) → Set _ Isomorphism f = Σ (B → A) λ g → AreInverses f g @@ -28,6 +30,21 @@ module _ {ℓa ℓb : Level} where _≅_ : Set ℓa → Set ℓb → Set _ A ≅ B = Σ (A → B) Isomorphism +module _ {ℓ : Level} {A B : Set ℓ} {f : A → B} + (g : B → A) (s : {A B : Set ℓ} → isSet (A → B)) where + + propAreInverses : isProp (AreInverses {A = A} {B} f g) + propAreInverses x y i = record + { verso-recto = ve-re + ; recto-verso = re-ve + } + where + open AreInverses + ve-re : g ∘ f ≡ idFun A + ve-re = s (g ∘ f) (idFun A) (verso-recto x) (verso-recto y) i + re-ve : f ∘ g ≡ idFun B + re-ve = s (f ∘ g) (idFun B) (recto-verso x) (recto-verso y) 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 @@ -130,54 +147,18 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open import Cubical.PathPrelude renaming (_≃_ to _≃η_) open import Cubical.Univalence using (_≃_) + + doEta : A ≃ B → A ≃η B + doEta (_≃_.con eqv isEqv) = eqv , isEqv + + deEta : A ≃η B → A ≃ B + deEta (eqv , isEqv) = _≃_.con eqv isEqv + 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 + open Equivalence (doEta 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 {!!} From 2058154c6523b6a3bd7cf2cd8435eae13b6defb1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 19 Mar 2018 15:15:03 +0100 Subject: [PATCH 08/38] Helpers to work with isomorphisms and equivalences --- src/Cat/Categories/Sets.agda | 10 +++++-- src/Cat/Equivalence.agda | 57 ++++++++++++++++++++++++++++++++++-- 2 files changed, 62 insertions(+), 5 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 5de99e3..13f8f98 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -18,9 +18,13 @@ open import Cat.Wishlist open import Cat.Equivalence as Eqv renaming (module NoEta to Eeq) using (AreInverses) module Equivalence = Eeq.Equivalence′ -postulate - _⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C - sym≃ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A ≃ B → B ≃ A + +_⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C +eqA ⊙ eqB = Equivalence.compose eqA eqB + +sym≃ : ∀ {ℓa ℓb} {A : Set ℓa} {B : Set ℓb} → A ≃ B → B ≃ A +sym≃ = Equivalence.symmetry + infixl 10 _⊙_ module _ (ℓ : Level) where diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index 62df900..795a25a 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -144,7 +144,48 @@ module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open AreInverses (snd iso) public -module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where + 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 ∎ + + 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) + + symmetryIso : B ≅ A + symmetryIso + = inverse + , obverse + , record + { verso-recto = recto-verso + ; recto-verso = verso-recto + } + + symmetry : B ≃ A + symmetry = B≃A.fromIsomorphism symmetryIso + where + module B≃A = Equiv≃ B A + +module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open import Cubical.PathPrelude renaming (_≃_ to _≃η_) open import Cubical.Univalence using (_≃_) @@ -154,8 +195,20 @@ module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where deEta : A ≃η B → A ≃ B deEta (eqv , isEqv) = _≃_.con eqv isEqv +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 - open Equivalence (doEta e) hiding (toIsomorphism ; fromIsomorphism ; _~_) public + open Equivalence (doEta e) hiding + ( toIsomorphism ; fromIsomorphism ; _~_ + ; compose ; symmetryIso ; symmetry ) public + + compose : {ℓc : Level} {C : Set ℓc} → (B ≃ C) → A ≃ C + compose ee = deEta (Equivalence.compose (doEta e) (doEta ee)) + + symmetry : B ≃ A + symmetry = deEta (Equivalence.symmetry (doEta e)) fromIsomorphism : A ≅ B → A ≃ B fromIsomorphism (f , iso) = _≃_.con f (Equiv≃.fromIso _ _ iso) From 43563d1ad93c8dfb972b694d6e6fd86d59db4430 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 19 Mar 2018 16:27:03 +0100 Subject: [PATCH 09/38] [WIP] Univalence for category of homotopy sets --- src/Cat/Categories/Sets.agda | 83 +++++++++++++++++++++++++++++++++--- 1 file changed, 76 insertions(+), 7 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 13f8f98..8aaa025 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -8,7 +8,7 @@ open import Function using (_∘_) -- open import Cubical using (funExt ; refl ; isSet ; isProp ; _≡_ ; isEquiv ; sym ; trans ; _[_≡_] ; I ; Path ; PathP) open import Cubical hiding (_≃_) -open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv) +open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua) open import Cubical.GradLemma open import Cat.Category @@ -27,6 +27,13 @@ sym≃ = Equivalence.symmetry infixl 10 _⊙_ +inv-coe : {ℓ : Level} {A B : Set ℓ} {a : A} + → (p : A ≡ B) → coe (sym p) (coe p a) ≡ a +inv-coe = {!!} +inv-coe' : {ℓ : Level} {A B : Set ℓ} {a : A} + → (p : B ≡ A) → coe p (coe (sym p) a) ≡ a +inv-coe' = {!!} + module _ (ℓ : Level) where private open import Cubical.NType.Properties @@ -89,11 +96,73 @@ module _ (ℓ : Level) where res : x ≡ y res i = 1eq i , 2eq i module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where - postulate - lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P) - → (p ≡ q) ≃ (proj₁ p ≡ proj₁ q) - lem3 : {Q : A → Set ℓb} → ((x : A) → P x ≃ Q x) - → Σ A P ≃ Σ A Q + lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P) + → (p ≡ q) ≃ (proj₁ p ≡ proj₁ q) + lem2 pA p q = Eeq.fromIsomorphism iso + where + f : p ≡ q → proj₁ p ≡ proj₁ q + f e i = proj₁ (e i) + g : proj₁ p ≡ proj₁ q → p ≡ q + g = lemSig pA p q + ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e + -- QUESTION Why does `h` not satisfy the constraint here? + ve-re e i j = qq0 j , {!h!} + where + -- qq : ? [ proj₂ ((g ∘ f) e) ≡ proj₂ e ] + qq0 : proj₁ p ≡ proj₁ q + qq0 i = proj₁ (e i) + qq : (λ i → P (qq0 i)) [ proj₂ p ≡ proj₂ q ] + qq = lemPropF pA qq0 + h : P (qq0 j) + h = qq j + re-ve : (e : proj₁ p ≡ proj₁ q) → (f ∘ g) e ≡ e + re-ve e = refl + inv : AreInverses f g + inv = record + { verso-recto = funExt ve-re + ; recto-verso = funExt re-ve + } + iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q) + iso = f , g , inv + + lem3 : {Q : A → Set ℓb} → ((a : A) → P a ≃ Q a) + → Σ A P ≃ Σ A Q + lem3 {Q} eA = res + where + P→Q : ∀ {a} → P a ≡ Q a + P→Q = ua (eA _) + Q→P : ∀ {a} → Q a ≡ P a + Q→P = sym P→Q + f : Σ A P → Σ A Q + f (a , pA) = a , coe P→Q pA + g : Σ A Q → Σ A P + g (a , qA) = a , coe Q→P qA + ve-re : (x : Σ A P) → (g ∘ f) x ≡ x + ve-re x i = proj₁ x , eq i + where + eq : proj₂ ((g ∘ f) x) ≡ proj₂ x + eq = begin + proj₂ ((g ∘ f) x) ≡⟨⟩ + coe Q→P (proj₂ (f x)) ≡⟨⟩ + coe Q→P (coe P→Q (proj₂ x)) ≡⟨ inv-coe P→Q ⟩ + proj₂ x ∎ + re-ve : (x : Σ A Q) → (f ∘ g) x ≡ x + re-ve x i = proj₁ x , eq i + where + eq = begin + proj₂ ((f ∘ g) x) ≡⟨⟩ + coe P→Q (coe Q→P (proj₂ x)) ≡⟨⟩ + coe P→Q (coe (sym P→Q) (proj₂ x)) ≡⟨ inv-coe' P→Q ⟩ + proj₂ x ∎ + inv : AreInverses f g + inv = record + { verso-recto = funExt ve-re + ; recto-verso = funExt re-ve + } + iso : Σ A P Eqv.≅ Σ A Q + iso = f , g , inv + res : Σ A P ≃ Σ A Q + res = Eeq.fromIsomorphism iso module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where postulate @@ -136,7 +205,7 @@ module _ (ℓ : Level) where res = _≃_.isEqv t module _ {hA hB : hSet {ℓ}} where univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) - univalent = let k = _≃_.isEqv (sym≃ conclusion) in {!!} + univalent = let k = _≃_.isEqv (sym≃ conclusion) in {!k!} SetsIsCategory : IsCategory SetsRaw IsCategory.isAssociative SetsIsCategory = refl From 32d1833d517a9c1aceee97bfcafedbfa5c01fbfc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 11:26:48 +0100 Subject: [PATCH 10/38] [WIP] A long way towards proving univalence in the category of hSets --- src/Cat/Categories/Sets.agda | 86 ++++++++++++++++++++++++++++-------- src/Cat/Equivalence.agda | 44 +++++++++++++++++- 2 files changed, 110 insertions(+), 20 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 8aaa025..cc3d655 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -15,7 +15,7 @@ open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product open import Cat.Wishlist -open import Cat.Equivalence as Eqv renaming (module NoEta to Eeq) using (AreInverses) +open import Cat.Equivalence as Eqv renaming (module NoEta to Eeq) using (AreInverses ; module Equiv≃) module Equivalence = Eeq.Equivalence′ @@ -27,12 +27,33 @@ sym≃ = Equivalence.symmetry infixl 10 _⊙_ -inv-coe : {ℓ : Level} {A B : Set ℓ} {a : A} - → (p : A ≡ B) → coe (sym p) (coe p a) ≡ a -inv-coe = {!!} -inv-coe' : {ℓ : Level} {A B : Set ℓ} {a : A} - → (p : B ≡ A) → coe p (coe (sym p) a) ≡ a -inv-coe' = {!!} +module _ {ℓ : Level} {A : Set ℓ} {a : A} where + id-coe : coe refl a ≡ a + id-coe = begin + coe refl a ≡⟨ {!!} ⟩ + a ∎ + +module _ {ℓ : Level} {A B : Set ℓ} {a : A} where + inv-coe : (p : A ≡ B) → coe (sym p) (coe p a) ≡ a + inv-coe p = + let + D : (y : Set ℓ) → _ ≡ y → Set _ + D _ q = coe (sym q) (coe q a) ≡ a + d : D A refl + d = begin + coe (sym refl) (coe refl a) ≡⟨⟩ + coe refl (coe refl a) ≡⟨ id-coe ⟩ + coe refl a ≡⟨ id-coe ⟩ + a ∎ + in pathJ D d B p + inv-coe' : (p : B ≡ A) → coe p (coe (sym p) a) ≡ a + inv-coe' p = + let + D : (y : Set ℓ) → _ ≡ y → Set _ + D _ q = coe (sym q) (coe q a) ≡ a + k : coe p (coe (sym p) a) ≡ a + k = pathJ D (trans id-coe id-coe) B (sym p) + in k module _ (ℓ : Level) where private @@ -125,8 +146,8 @@ module _ (ℓ : Level) where iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q) iso = f , g , inv - lem3 : {Q : A → Set ℓb} → ((a : A) → P a ≃ Q a) - → Σ A P ≃ Σ A Q + lem3 : {Q : A → Set ℓb} + → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q lem3 {Q} eA = res where P→Q : ∀ {a} → P a ≡ Q a @@ -165,9 +186,25 @@ module _ (ℓ : Level) where res = Eeq.fromIsomorphism iso module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where - postulate - lem4 : isSet A → isSet B → (f : A → B) - → isEquiv A B f ≃ isIso f + lem4 : isSet A → isSet B → (f : A → B) + → isEquiv A B f ≃ isIso f + lem4 sA sB f = + let + obv : isEquiv A B f → isIso f + obv = Equiv≃.toIso A B + inv : isIso 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 : isIso f) → (obv ∘ inv) x ≡ x + ve-re = Equiv≃.inverse-to-from-iso A B + iso : isEquiv A B f Eqv.≅ isIso f + iso = obv , inv , + record + { verso-recto = funExt re-ve + ; recto-verso = funExt ve-re + } + in Eeq.fromIsomorphism iso module _ {hA hB : Object} where private @@ -176,13 +213,24 @@ module _ (ℓ : Level) where B = proj₁ hB sB = proj₂ hB - postulate - -- lem3 and the equivalence from lem4 - step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) - -- univalence - step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) - -- lem2 with propIsSet - step2 : (A ≡ B) ≃ (hA ≡ hB) + + -- lem3 and the equivalence from lem4 + step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) + step0 = lem3 (λ f → sym≃ (lem4 sA sB f)) + -- univalence + step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) + step1 = + let + h : (A ≃ B) ≃ (A ≡ B) + h = sym≃ (univalence {A = A} {B}) + k : Σ _ (isEquiv (A ≃ B) (A ≡ B)) + k = Eqv.doEta h + in {!!} + + -- lem2 with propIsSet + step2 : (A ≡ B) ≃ (hA ≡ hB) + step2 = sym≃ (lem2 (λ A → isSetIsProp) hA hB) + -- Go from an isomorphism on sets to an isomorphism on homotopic sets trivial? : (hA ≅ hB) ≃ Σ (A → B) isIso trivial? = sym≃ (Eeq.fromIsomorphism res) diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index 795a25a..c047330 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -58,6 +58,23 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where _~_ : Set ℓa → Set ℓb → Set _ A ~ B = Σ _ iseqv + inverse-from-to-iso : ∀ {f} (x : _) → (fromIso {f} ∘ toIso {f}) x ≡ x + inverse-from-to-iso x = begin + (fromIso ∘ toIso) x ≡⟨⟩ + fromIso (toIso x) ≡⟨ propIsEquiv _ (fromIso (toIso x)) x ⟩ + x ∎ + + -- `toIso` is abstract - so I probably can't close this proof. + -- inverse-to-from-iso : ∀ {f} → toIso {f} ∘ fromIso {f} ≡ idFun _ + -- inverse-to-from-iso = funExt (λ x → begin + -- (toIso ∘ fromIso) x ≡⟨⟩ + -- toIso (fromIso x) ≡⟨ cong toIso (propIsEquiv _ (fromIso x) y) ⟩ + -- toIso y ≡⟨ {!!} ⟩ + -- x ∎) + -- where + -- y : iseqv _ + -- y = {!!} + fromIsomorphism : A ≅ B → A ~ B fromIsomorphism (f , iso) = f , fromIso iso @@ -130,7 +147,26 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where where import Cubical.NType.Properties as P - module Equiv≃ = Equiv ≃isEquiv + module Equiv≃ where + open Equiv ≃isEquiv public + inverse-to-from-iso : ∀ {f} (x : _) → (toIso {f} ∘ fromIso {f}) x ≡ x + inverse-to-from-iso {f} x = begin + (toIso ∘ fromIso) x ≡⟨⟩ + toIso (fromIso x) ≡⟨ cong toIso (propIsEquiv _ (fromIso x) y) ⟩ + toIso y ≡⟨ py ⟩ + x ∎ + where + helper : (x : Isomorphism _) → Σ _ λ y → toIso y ≡ x + helper (f~ , inv) = y , py + where + module inv = AreInverses inv + y : isEquiv _ _ f + y = {!!} + py : toIso y ≡ (f~ , inv) + py = {!!} + y : isEquiv _ _ _ + y = fst (helper x) + py = snd (helper x) module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open Cubical.PathPrelude using (_≃_) @@ -210,6 +246,12 @@ module NoEta {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where symmetry : B ≃ A symmetry = deEta (Equivalence.symmetry (doEta e)) + -- fromIso : {f : A → B} → Isomorphism f → isEquiv f + -- fromIso = ? + + -- toIso : {f : A → B} → isEquiv f → Isomorphism f + -- toIso = ? + fromIsomorphism : A ≅ B → A ≃ B fromIsomorphism (f , iso) = _≃_.con f (Equiv≃.fromIso _ _ iso) From 30725d71b6552d97882626cdcfcb0d202613ca54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 11:58:54 +0100 Subject: [PATCH 11/38] [WIP] Scary goal --- src/Cat/Categories/Sets.agda | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index cc3d655..1e92b60 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -28,10 +28,21 @@ sym≃ = Equivalence.symmetry infixl 10 _⊙_ module _ {ℓ : Level} {A : Set ℓ} {a : A} where + -- "This follows from the propositional equiality for `J`" - Vezzosi. id-coe : coe refl a ≡ a id-coe = begin - coe refl a ≡⟨ {!!} ⟩ + coe refl a ≡⟨⟩ + -- pathJprop : pathJ _ refl ≡ d + pathJ (λ y x → A) scary A refl ≡⟨ pathJprop {x = scary} (λ y x → A) scary ⟩ + scary ≡⟨ {!!} ⟩ + -- pathJ (λ y x → A) scary A refl ≡⟨ pathJprop {A = A} (λ y x → A) scary ⟩ + -- scary ≡⟨ {!!} ⟩ + + -- pathJ (λ y _ → B _ → B y) (λ x → x) _ p ≡⟨ {!!} ⟩ a ∎ + where + scary : A + scary = (primComp (λ j → A) i0 (λ j → p[ a ] i0 (~ j)) a) module _ {ℓ : Level} {A B : Set ℓ} {a : A} where inv-coe : (p : A ≡ B) → coe (sym p) (coe p a) ≡ a @@ -225,7 +236,11 @@ module _ (ℓ : Level) where h = sym≃ (univalence {A = A} {B}) k : Σ _ (isEquiv (A ≃ B) (A ≡ B)) k = Eqv.doEta h - in {!!} + eqv : Σ (A → B) (isEquiv A B) Eqv.≅ (A ≃ B) + eqv = {!!} , {!!} , {!!} + hh : Σ (A → B) (isEquiv A B) ≃ (A ≃ B) + hh = Eeq.fromIsomorphism eqv + in hh ⊙ h -- lem2 with propIsSet step2 : (A ≡ B) ≃ (hA ≡ hB) From 2188e690a0d86ad6de3221bb38c4f50331a7658e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 12:12:09 +0100 Subject: [PATCH 12/38] Prove identity law for coercions. --- src/Cat/Categories/Sets.agda | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 1e92b60..b8c83e5 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -28,21 +28,12 @@ sym≃ = Equivalence.symmetry infixl 10 _⊙_ module _ {ℓ : Level} {A : Set ℓ} {a : A} where - -- "This follows from the propositional equiality for `J`" - Vezzosi. id-coe : coe refl a ≡ a id-coe = begin coe refl a ≡⟨⟩ - -- pathJprop : pathJ _ refl ≡ d - pathJ (λ y x → A) scary A refl ≡⟨ pathJprop {x = scary} (λ y x → A) scary ⟩ - scary ≡⟨ {!!} ⟩ - -- pathJ (λ y x → A) scary A refl ≡⟨ pathJprop {A = A} (λ y x → A) scary ⟩ - -- scary ≡⟨ {!!} ⟩ - - -- pathJ (λ y _ → B _ → B y) (λ x → x) _ p ≡⟨ {!!} ⟩ + pathJ (λ y x → A) _ A refl ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩ + _ ≡⟨ pathJprop {x = a} (λ y x → A) _ ⟩ a ∎ - where - scary : A - scary = (primComp (λ j → A) i0 (λ j → p[ a ] i0 (~ j)) a) module _ {ℓ : Level} {A B : Set ℓ} {a : A} where inv-coe : (p : A ≡ B) → coe (sym p) (coe p a) ≡ a From 66cb5b363dcce2edd2f211ad1ebef5ba3acc8c8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 13:26:40 +0100 Subject: [PATCH 13/38] [WIP] Finnish all intermediate steps for univalence of hSets --- src/Cat/Categories/Sets.agda | 20 ++++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index b8c83e5..0c7f420 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -221,17 +221,25 @@ module _ (ℓ : Level) where step0 = lem3 (λ f → sym≃ (lem4 sA sB f)) -- univalence step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) - step1 = - let + step1 = hh ⊙ h + where h : (A ≃ B) ≃ (A ≡ B) h = sym≃ (univalence {A = A} {B}) - k : Σ _ (isEquiv (A ≃ B) (A ≡ B)) - k = Eqv.doEta h + obv : Σ (A → B) (isEquiv A B) → A ≃ B + obv = Eqv.deEta + inv : A ≃ B → Σ (A → B) (isEquiv A B) + inv = Eqv.doEta + re-ve : (x : _) → (inv ∘ obv) x ≡ x + re-ve x = refl + -- Because _≃_ does not have eta equality! + ve-re : (x : _) → (obv ∘ inv) x ≡ x + ve-re (con eqv isEqv) i = con eqv isEqv + areInv : AreInverses obv inv + areInv = record { verso-recto = funExt re-ve ; recto-verso = funExt ve-re } eqv : Σ (A → B) (isEquiv A B) Eqv.≅ (A ≃ B) - eqv = {!!} , {!!} , {!!} + eqv = obv , inv , areInv hh : Σ (A → B) (isEquiv A B) ≃ (A ≃ B) hh = Eeq.fromIsomorphism eqv - in hh ⊙ h -- lem2 with propIsSet step2 : (A ≡ B) ≃ (hA ≡ hB) From b03bfb0c777ecfaec51b39dc9b6039de09b272f3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 14:58:27 +0100 Subject: [PATCH 14/38] Restructure in free monad --- src/Cat/Categories/Free.agda | 88 +++++++++++++++++++++--------------- src/Cat/Categories/Sets.agda | 4 +- src/Cat/Category/Monoid.agda | 2 +- 3 files changed, 55 insertions(+), 39 deletions(-) diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 7e80478..b227c5d 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -2,61 +2,77 @@ module Cat.Categories.Free where open import Agda.Primitive -open import Cubical hiding (Path ; isSet ; empty) +open import Relation.Binary + +open import Cubical hiding (Path ; empty) open import Data.Product open import Cat.Category -data Path {ℓ ℓ' : Level} {A : Set ℓ} (R : A → A → Set ℓ') : (a b : A) → Set (ℓ ⊔ ℓ') where - empty : {a : A} → Path R a a - cons : {a b c : A} → R b c → Path R a b → Path R a c +module _ {ℓ : Level} {A : Set ℓ} {ℓr : Level} where + data Path (R : Rel A ℓr) : (a b : A) → Set (ℓ ⊔ ℓr) where + empty : {a : A} → Path R a a + cons : {a b c : A} → R b c → Path R a b → Path R a c -concatenate _++_ : ∀ {ℓ ℓ'} {A : Set ℓ} {a b c : A} {R : A → A → Set ℓ'} → Path R b c → Path R a b → Path R a c -concatenate empty p = p -concatenate (cons x q) p = cons x (concatenate q p) -_++_ = concatenate + module _ {R : Rel A ℓr} where + concatenate : {a b c : A} → Path R b c → Path R a b → Path R a c + concatenate empty p = p + concatenate (cons x q) p = cons x (concatenate q p) + _++_ : {a b c : A} → Path R b c → Path R a b → Path R a c + a ++ b = concatenate a b -singleton : ∀ {ℓ} {𝓤 : Set ℓ} {ℓr} {R : 𝓤 → 𝓤 → Set ℓr} {A B : 𝓤} → R A B → Path R A B -singleton f = cons f empty + singleton : {a b : A} → R a b → Path R a b + singleton f = cons f empty -module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where +module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where private module ℂ = Category ℂ - open Category ℂ - p-isAssociative : {A B C D : Object} {r : Path Arrow A B} {q : Path Arrow B C} {p : Path Arrow C D} + RawFree : RawCategory ℓa (ℓa ⊔ ℓb) + RawCategory.Object RawFree = ℂ.Object + RawCategory.Arrow RawFree = Path ℂ.Arrow + RawCategory.𝟙 RawFree = empty + RawCategory._∘_ RawFree = concatenate + + open RawCategory RawFree + open Univalence RawFree + + + isAssociative : {A B C D : ℂ.Object} {r : Path ℂ.Arrow A B} {q : Path ℂ.Arrow B C} {p : Path ℂ.Arrow C D} → p ++ (q ++ r) ≡ (p ++ q) ++ r - p-isAssociative {r = r} {q} {empty} = refl - p-isAssociative {A} {B} {C} {D} {r = r} {q} {cons x p} = begin + isAssociative {r = r} {q} {empty} = refl + isAssociative {A} {B} {C} {D} {r = r} {q} {cons x p} = begin cons x p ++ (q ++ r) ≡⟨ cong (cons x) lem ⟩ cons x ((p ++ q) ++ r) ≡⟨⟩ (cons x p ++ q) ++ r ∎ where - lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r) - lem = p-isAssociative {r = r} {q} {p} + lem : p ++ (q ++ r) ≡ ((p ++ q) ++ r) + lem = isAssociative {r = r} {q} {p} - ident-r : ∀ {A} {B} {p : Path Arrow A B} → concatenate p empty ≡ p + ident-r : ∀ {A} {B} {p : Path ℂ.Arrow A B} → concatenate p empty ≡ p ident-r {p = empty} = refl ident-r {p = cons x p} = cong (cons x) ident-r - ident-l : ∀ {A} {B} {p : Path Arrow A B} → concatenate empty p ≡ p + ident-l : ∀ {A} {B} {p : Path ℂ.Arrow A B} → concatenate empty p ≡ p ident-l = refl - module _ {A B : Object} where - isSet : Cubical.isSet (Path Arrow A B) - isSet a b p q = {!!} + isIdentity : IsIdentity 𝟙 + isIdentity = ident-r , ident-l - RawFree : RawCategory ℓ (ℓ ⊔ ℓ') - RawFree = record - { Object = Object - ; Arrow = Path Arrow - ; 𝟙 = empty - ; _∘_ = concatenate - } - RawIsCategoryFree : IsCategory RawFree - RawIsCategoryFree = record - { isAssociative = λ { {f = f} {g} {h} → p-isAssociative {r = f} {g} {h}} - ; isIdentity = ident-r , ident-l - ; arrowsAreSets = {!!} - ; univalent = {!!} - } + module _ {A B : ℂ.Object} where + arrowsAreSets : Cubical.isSet (Path ℂ.Arrow A B) + arrowsAreSets a b p q = {!!} + + eqv : isEquiv (A ≡ B) (A ≅ B) (id-to-iso isIdentity A B) + eqv = {!!} + univalent : Univalent isIdentity + univalent = eqv + + isCategory : IsCategory RawFree + IsCategory.isAssociative isCategory {f = f} {g} {h} = isAssociative {r = f} {g} {h} + IsCategory.isIdentity isCategory = isIdentity + IsCategory.arrowsAreSets isCategory = arrowsAreSets + IsCategory.univalent isCategory = univalent + + Free : Category _ _ + Free = record { raw = RawFree ; isCategory = isCategory } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 0c7f420..54050d8 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -10,6 +10,7 @@ open import Function using (_∘_) open import Cubical hiding (_≃_) open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua) open import Cubical.GradLemma +open import Cubical.NType.Properties open import Cat.Category open import Cat.Category.Functor @@ -59,8 +60,7 @@ module _ {ℓ : Level} {A B : Set ℓ} {a : A} where module _ (ℓ : Level) where private - open import Cubical.NType.Properties - open import Cubical.Universe + open import Cubical.Universe using (hSet) public SetsRaw : RawCategory (lsuc ℓ) ℓ RawCategory.Object SetsRaw = hSet {ℓ} diff --git a/src/Cat/Category/Monoid.agda b/src/Cat/Category/Monoid.agda index a17468e..75eaa68 100644 --- a/src/Cat/Category/Monoid.agda +++ b/src/Cat/Category/Monoid.agda @@ -19,7 +19,7 @@ module _ (ℓa ℓb : Level) where -- -- Since it doesn't we'll make the following (definitionally equivalent) ad-hoc definition. _×_ : ∀ {ℓa ℓb} → Category ℓa ℓb → Category ℓa ℓb → Category ℓa ℓb - ℂ × 𝔻 = Cat.CatProduct.obj ℂ 𝔻 + ℂ × 𝔻 = Cat.CatProduct.object ℂ 𝔻 record RawMonoidalCategory : Set ℓ where field From 811a6bf58e64168b545718448e8c955fac4d5bd5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 15:19:28 +0100 Subject: [PATCH 15/38] Make univalence a submodule of RawCategory --- src/Cat/Categories/Cat.agda | 3 ++- src/Cat/Categories/Free.agda | 9 +++++---- src/Cat/Categories/Fun.agda | 7 ++++--- src/Cat/Categories/Sets.agda | 5 +++-- src/Cat/Category.agda | 26 ++++++++++++-------------- 5 files changed, 26 insertions(+), 24 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index f013c82..f429985 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -97,7 +97,8 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where isIdentity = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity) , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity) - postulate univalent : Univalence.Univalent rawProduct isIdentity + + postulate univalent : Univalence.Univalent isIdentity instance isCategory : IsCategory rawProduct IsCategory.isAssociative isCategory = Σ≡ ℂ.isAssociative 𝔻.isAssociative diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index b227c5d..9d8d3d4 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -35,8 +35,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where RawCategory._∘_ RawFree = concatenate open RawCategory RawFree - open Univalence RawFree - isAssociative : {A B C D : ℂ.Object} {r : Path ℂ.Arrow A B} {q : Path ℂ.Arrow B C} {p : Path ℂ.Arrow C D} → p ++ (q ++ r) ≡ (p ++ q) ++ r @@ -59,13 +57,16 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where isIdentity : IsIdentity 𝟙 isIdentity = ident-r , ident-l + open Univalence isIdentity + module _ {A B : ℂ.Object} where arrowsAreSets : Cubical.isSet (Path ℂ.Arrow A B) arrowsAreSets a b p q = {!!} - eqv : isEquiv (A ≡ B) (A ≅ B) (id-to-iso isIdentity A B) + eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso isIdentity A B) eqv = {!!} - univalent : Univalent isIdentity + + univalent : Univalent univalent = eqv isCategory : IsCategory RawFree diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 019e8b6..4c020cb 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -67,7 +67,8 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C } open RawCategory RawFun - open Univalence RawFun + open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f}) + module _ {A B : Functor ℂ 𝔻} where module A = Functor A module B = Functor B @@ -145,10 +146,10 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C re-ve : (x : A ≡ B) → reverse (obverse x) ≡ x re-ve = {!!} - done : isEquiv (A ≡ B) (A ≅ B) (id-to-iso (λ { {A} {B} → isIdentity {A} {B}}) A B) + done : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso (λ { {A} {B} → isIdentity {A} {B}}) A B) done = {!gradLemma obverse reverse ve-re re-ve!} - univalent : Univalent (λ{ {A} {B} → isIdentity {A} {B}}) + univalent : Univalent univalent = done instance diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 54050d8..e7e2024 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -69,12 +69,13 @@ module _ (ℓ : Level) where RawCategory._∘_ SetsRaw = Function._∘′_ open RawCategory SetsRaw hiding (_∘_) - open Univalence SetsRaw isIdentity : IsIdentity Function.id proj₁ isIdentity = funExt λ _ → refl proj₂ isIdentity = funExt λ _ → refl + open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f}) + arrowsAreSets : ArrowsAreSets arrowsAreSets {B = (_ , s)} = setPi λ _ → s @@ -266,7 +267,7 @@ module _ (ℓ : Level) where res : isEquiv (hA ≡ hB) (hA ≅ hB) (_≃_.eqv t) res = _≃_.isEqv t module _ {hA hB : hSet {ℓ}} where - univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) + univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) univalent = let k = _≃_.isEqv (sym≃ conclusion) in {!k!} SetsIsCategory : IsCategory SetsRaw diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 5b84a79..834ff47 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -129,12 +129,8 @@ 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. --- --- 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 + -- | Univalence is indexed by a raw category as well as an identity proof. + module Univalence (isIdentity : IsIdentity 𝟙) where idIso : (A : Object) → A ≅ A idIso A = 𝟙 , (𝟙 , isIdentity) @@ -162,12 +158,13 @@ module Univalence {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where -- [HoTT]. record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc (ℓa ⊔ ℓb)) where open RawCategory ℂ public - open Univalence ℂ public field isAssociative : IsAssociative isIdentity : IsIdentity 𝟙 arrowsAreSets : ArrowsAreSets - univalent : Univalent isIdentity + open Univalence isIdentity public + field + univalent : Univalent -- Some common lemmas about categories. module _ {A B : Object} {X : Object} (f : Arrow A B) where @@ -243,7 +240,7 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where 𝟙 ∘ g' ≡⟨ snd isIdentity ⟩ g' ∎ - propUnivalent : isProp (Univalent isIdentity) + propUnivalent : isProp Univalent propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i private @@ -251,7 +248,7 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where module IC = IsCategory module X = IsCategory x module Y = IsCategory y - open Univalence ℂ + open Univalence -- In a few places I use the result of propositionality of the various -- projections of `IsCategory` - I've arbitrarily chosed to use this -- result from `x : IsCategory C`. I don't know which (if any) possibly @@ -336,21 +333,22 @@ module Opposite {ℓa ℓb : Level} where RawCategory._∘_ opRaw = Function.flip ℂ._∘_ open RawCategory opRaw - open Univalence opRaw isIdentity : IsIdentity 𝟙 isIdentity = swap ℂ.isIdentity + open Univalence isIdentity + module _ {A B : ℂ.Object} where univalent : isEquiv (A ≡ B) (A ≅ B) - (id-to-iso (swap ℂ.isIdentity) A B) + (Univalence.id-to-iso (swap ℂ.isIdentity) A B) fst (univalent iso) = flipFiber (fst (ℂ.univalent (flipIso iso))) where flipIso : A ≅ B → B ℂ.≅ A flipIso (f , f~ , iso) = f , f~ , swap iso flipFiber - : fiber (ℂ.id-to-iso ℂ.isIdentity B A) (flipIso iso) - → fiber ( id-to-iso isIdentity A B) iso + : fiber (ℂ.id-to-iso B A) (flipIso iso) + → fiber ( id-to-iso A B) iso flipFiber (eq , eqIso) = sym eq , {!!} snd (univalent iso) = {!!} From 63a51fbfdc16bcc96db848bddccfe41fee972400 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 16:08:37 +0100 Subject: [PATCH 16/38] Include modules in "everything"-module --- src/Cat.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/Cat.agda b/src/Cat.agda index 86e6879..80d101d 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -8,7 +8,10 @@ open import Cat.Category.Exponential open import Cat.Category.CartesianClosed open import Cat.Category.NaturalTransformation open import Cat.Category.Yoneda +open import Cat.Category.Monoid open import Cat.Category.Monad +open Cat.Category.Monad.Monoidal +open Cat.Category.Monad.Kleisli open import Cat.Category.Monad.Voevodsky open import Cat.Categories.Sets From b6a9befd9c0c2be952ee128203b225bf7729b0db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 16:26:23 +0100 Subject: [PATCH 17/38] Naming and formatting --- src/Cat/Category/Functor.agda | 67 +++++++++++---------- src/Cat/Category/NaturalTransformation.agda | 9 ++- 2 files changed, 40 insertions(+), 36 deletions(-) diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index fc23c2e..44b560e 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -2,9 +2,11 @@ module Cat.Category.Functor where open import Agda.Primitive -open import Cubical open import Function +open import Cubical +open import Cubical.NType.Properties using (lemPropF) + open import Cat.Category open Category hiding (_∘_ ; raw ; IsIdentity) @@ -72,8 +74,6 @@ module _ {ℓc ℓc' ℓd ℓd'} open IsFunctor isFunctor public -open Functor - EndoFunctor : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → Set _ EndoFunctor ℂ = Functor ℂ ℂ @@ -87,7 +87,7 @@ module _ propIsFunctor : isProp (IsFunctor _ _ F) propIsFunctor isF0 isF1 i = record - { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i + { isIdentity = 𝔻.arrowsAreSets _ _ isF0.isIdentity isF1.isIdentity i ; isDistributive = 𝔻.arrowsAreSets _ _ isF0.isDistributive isF1.isDistributive i } where @@ -108,15 +108,14 @@ module _ IsFunctorIsProp' : IsProp' λ i → IsFunctor _ _ (F i) IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻} (\ F → propIsFunctor F) (\ i → F i) - where - open import Cubical.NType.Properties using (lemPropF) module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where + open Functor Functor≡ : {F G : Functor ℂ 𝔻} - → raw F ≡ raw G + → Functor.raw F ≡ Functor.raw G → F ≡ G - raw (Functor≡ eq i) = eq i - isFunctor (Functor≡ {F} {G} eq i) + Functor.raw (Functor≡ eq i) = eq i + Functor.isFunctor (Functor≡ {F} {G} eq i) = res i where res : (λ i → IsFunctor ℂ 𝔻 (eq i)) [ isFunctor F ≡ isFunctor G ] @@ -124,35 +123,37 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where private - F* = omap F - F→ = fmap F - G* = omap G - G→ = fmap G + module F = Functor F + module G = Functor G module _ {a0 a1 a2 : Object A} {α0 : A [ a0 , a1 ]} {α1 : A [ a1 , a2 ]} where - - dist : (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡ C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] + dist : (F.fmap ∘ G.fmap) (A [ α1 ∘ α0 ]) ≡ C [ (F.fmap ∘ G.fmap) α1 ∘ (F.fmap ∘ G.fmap) α0 ] dist = begin - (F→ ∘ G→) (A [ α1 ∘ α0 ]) ≡⟨ refl ⟩ - F→ (G→ (A [ α1 ∘ α0 ])) ≡⟨ cong F→ (isDistributive G) ⟩ - F→ (B [ G→ α1 ∘ G→ α0 ]) ≡⟨ isDistributive F ⟩ - C [ (F→ ∘ G→) α1 ∘ (F→ ∘ G→) α0 ] ∎ + (F.fmap ∘ G.fmap) (A [ α1 ∘ α0 ]) + ≡⟨ refl ⟩ + F.fmap (G.fmap (A [ α1 ∘ α0 ])) + ≡⟨ cong F.fmap G.isDistributive ⟩ + F.fmap (B [ G.fmap α1 ∘ G.fmap α0 ]) + ≡⟨ F.isDistributive ⟩ + C [ (F.fmap ∘ G.fmap) α1 ∘ (F.fmap ∘ G.fmap) α0 ] + ∎ - _∘fr_ : RawFunctor A C - RawFunctor.omap _∘fr_ = F* ∘ G* - RawFunctor.fmap _∘fr_ = F→ ∘ G→ - instance - isFunctor' : IsFunctor A C _∘fr_ - isFunctor' = record - { isIdentity = begin - (F→ ∘ G→) (𝟙 A) ≡⟨ refl ⟩ - F→ (G→ (𝟙 A)) ≡⟨ cong F→ (isIdentity G)⟩ - F→ (𝟙 B) ≡⟨ isIdentity F ⟩ - 𝟙 C ∎ - ; isDistributive = dist - } + raw : RawFunctor A C + RawFunctor.omap raw = F.omap ∘ G.omap + RawFunctor.fmap raw = F.fmap ∘ G.fmap + + isFunctor : IsFunctor A C raw + isFunctor = record + { isIdentity = begin + (F.fmap ∘ G.fmap) (𝟙 A) ≡⟨ refl ⟩ + F.fmap (G.fmap (𝟙 A)) ≡⟨ cong F.fmap (G.isIdentity)⟩ + F.fmap (𝟙 B) ≡⟨ F.isIdentity ⟩ + 𝟙 C ∎ + ; isDistributive = dist + } F[_∘_] : Functor A C - raw F[_∘_] = _∘fr_ + Functor.raw F[_∘_] = raw + Functor.isFunctor F[_∘_] = isFunctor -- The identity functor identity : ∀ {ℓ ℓ'} → {C : Category ℓ ℓ'} → Functor C C diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index dea2e50..2ccef94 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -113,8 +113,11 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level} lem : (λ _ → Natural F G θ) [ (λ f → θNat f) ≡ (λ f → θNat' f) ] lem = λ i f → 𝔻.arrowsAreSets _ _ (θNat f) (θNat' f) i - naturalTransformationIsSet : isSet (NaturalTransformation F G) - naturalTransformationIsSet = sigPresSet transformationIsSet - λ θ → ntypeCommulative + naturalIsSet : (θ : Transformation F G) → isSet (Natural F G θ) + naturalIsSet θ = + ntypeCommulative (s≤s {n = Nat.suc Nat.zero} z≤n) (naturalIsProp θ) + + naturalTransformationIsSet : isSet (NaturalTransformation F G) + naturalTransformationIsSet = sigPresSet transformationIsSet naturalIsSet From 629115661b891c0f398c4d90a4f725cc940c8832 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 16:43:48 +0100 Subject: [PATCH 18/38] Formatting in yoneda --- src/Cat/Category/Yoneda.agda | 43 ++++++++++++++++++------------------ 1 file changed, 22 insertions(+), 21 deletions(-) diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index af7567a..d00a3ec 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -12,51 +12,52 @@ open import Cat.Category.Functor open import Cat.Equality open import Cat.Categories.Fun -open import Cat.Categories.Sets -open import Cat.Categories.Cat +open import Cat.Categories.Sets hiding (presheaf) + +-- There is no (small) category of categories. So we won't use _⇑_ from +-- `HasExponential` +-- +-- open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_) +-- +-- In stead we'll use an ad-hoc definition -- which is definitionally equivalent +-- to that other one - even without mentioning the category of categories. +_⇑_ : {ℓ : Level} → Category ℓ ℓ → Category ℓ ℓ → Category ℓ ℓ +_⇑_ = Fun.Fun module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where private 𝓢 = Sets ℓ open Fun (opposite ℂ) 𝓢 - prshf = presheaf ℂ + presheaf = Cat.Categories.Sets.presheaf ℂ module ℂ = Category ℂ - -- There is no (small) category of categories. So we won't use _⇑_ from - -- `HasExponential` - -- - -- open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_) - -- - -- In stead we'll use an ad-hoc definition -- which is definitionally - -- equivalent to that other one. - _⇑_ = CatExponential.object - module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where - fmap : Transformation (prshf A) (prshf B) + fmap : Transformation (presheaf A) (presheaf B) fmap C x = ℂ [ f ∘ x ] - fmapNatural : Natural (prshf A) (prshf B) fmap + fmapNatural : Natural (presheaf A) (presheaf B) fmap fmapNatural g = funExt λ _ → ℂ.isAssociative - fmapNT : NaturalTransformation (prshf A) (prshf B) + fmapNT : NaturalTransformation (presheaf A) (presheaf B) fmapNT = fmap , fmapNatural rawYoneda : RawFunctor ℂ Fun - RawFunctor.omap rawYoneda = prshf + RawFunctor.omap rawYoneda = presheaf RawFunctor.fmap rawYoneda = fmapNT + open RawFunctor rawYoneda hiding (fmap) isIdentity : IsIdentity - isIdentity {c} = lemSig (naturalIsProp {F = prshf c} {prshf c}) _ _ eq + isIdentity {c} = lemSig (naturalIsProp {F = presheaf c} {presheaf c}) _ _ eq where - eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) + eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (presheaf c) eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity isDistributive : IsDistributive isDistributive {A} {B} {C} {f = f} {g} - = lemSig (propIsNatural (prshf A) (prshf C)) _ _ eq + = lemSig (propIsNatural (presheaf A) (presheaf C)) _ _ eq where - T[_∘_]' = T[_∘_] {F = prshf A} {prshf B} {prshf C} + T[_∘_]' = T[_∘_] {F = presheaf A} {presheaf B} {presheaf C} eqq : (X : ℂ.Object) → (x : ℂ [ X , A ]) → fmap (ℂ [ g ∘ f ]) X x ≡ T[ fmap g ∘ fmap f ]' X x eqq X x = begin @@ -76,5 +77,5 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where IsFunctor.isDistributive isFunctor = isDistributive yoneda : Functor ℂ Fun - Functor.raw yoneda = rawYoneda + Functor.raw yoneda = rawYoneda Functor.isFunctor yoneda = isFunctor From 31257a4d97576d4bba637fc4763fbff979f424ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 16:50:03 +0100 Subject: [PATCH 19/38] Do not export helpers in `Fun` --- src/Cat/Categories/Fun.agda | 79 ++++++++++++++++++------------------ src/Cat/Categories/Sets.agda | 4 +- src/Cat/Category/Yoneda.agda | 5 ++- 3 files changed, 46 insertions(+), 42 deletions(-) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 4c020cb..9bbb438 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -69,54 +69,55 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C open RawCategory RawFun open Univalence (λ {A} {B} {f} → isIdentity {A} {B} {f}) - module _ {A B : Functor ℂ 𝔻} where - module A = Functor A - module B = Functor B - module _ (p : A ≡ B) where - omapP : A.omap ≡ B.omap - omapP i = Functor.omap (p i) + private + module _ {A B : Functor ℂ 𝔻} where + module A = Functor A + module B = Functor B + module _ (p : A ≡ B) where + omapP : A.omap ≡ B.omap + omapP i = Functor.omap (p i) - coerceAB : ∀ {X} → 𝔻 [ A.omap X , A.omap X ] ≡ 𝔻 [ A.omap X , B.omap X ] - coerceAB {X} = cong (λ φ → 𝔻 [ A.omap X , φ X ]) omapP + coerceAB : ∀ {X} → 𝔻 [ A.omap X , A.omap X ] ≡ 𝔻 [ A.omap X , B.omap X ] + coerceAB {X} = cong (λ φ → 𝔻 [ A.omap X , φ X ]) omapP - -- The transformation will be the identity on 𝔻. Such an arrow has the - -- type `A.omap A → A.omap A`. Which we can coerce to have the type - -- `A.omap → B.omap` since `A` and `B` are equal. - coe𝟙 : Transformation A B - coe𝟙 X = coe coerceAB 𝔻.𝟙 + -- The transformation will be the identity on 𝔻. Such an arrow has the + -- type `A.omap A → A.omap A`. Which we can coerce to have the type + -- `A.omap → B.omap` since `A` and `B` are equal. + coe𝟙 : Transformation A B + coe𝟙 X = coe coerceAB 𝔻.𝟙 - module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where - nat' : 𝔻 [ coe𝟙 b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coe𝟙 a ] - nat' = begin - (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡⟨ {!!} ⟩ - (𝔻 [ B.fmap f ∘ coe𝟙 a ]) ∎ + module _ {a b : ℂ.Object} (f : ℂ [ a , b ]) where + nat' : 𝔻 [ coe𝟙 b ∘ A.fmap f ] ≡ 𝔻 [ B.fmap f ∘ coe𝟙 a ] + nat' = begin + (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡⟨ {!!} ⟩ + (𝔻 [ B.fmap f ∘ coe𝟙 a ]) ∎ - transs : (i : I) → Transformation A (p i) - transs = {!!} + transs : (i : I) → Transformation A (p i) + transs = {!!} - natt : (i : I) → Natural A (p i) {!!} - natt = {!!} + natt : (i : I) → Natural A (p i) {!!} + natt = {!!} - t : Natural A B coe𝟙 - t = coe c (identityNatural A) - where - c : Natural A A (identityTrans A) ≡ Natural A B coe𝟙 - c = begin - Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩ - Natural A B coe𝟙 ∎ - -- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!} + t : Natural A B coe𝟙 + t = coe c (identityNatural A) + where + c : Natural A A (identityTrans A) ≡ Natural A B coe𝟙 + c = begin + Natural A A (identityTrans A) ≡⟨ (λ x → {!natt ?!}) ⟩ + Natural A B coe𝟙 ∎ + -- cong (λ φ → {!Natural A A (identityTrans A)!}) {!!} - k : Natural A A (identityTrans A) → Natural A B coe𝟙 - k n {a} {b} f = res - where - res : (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coe𝟙 a ]) - res = {!!} + k : Natural A A (identityTrans A) → Natural A B coe𝟙 + k n {a} {b} f = res + where + res : (𝔻 [ coe𝟙 b ∘ A.fmap f ]) ≡ (𝔻 [ B.fmap f ∘ coe𝟙 a ]) + res = {!!} - nat : Natural A B coe𝟙 - nat = nat' + nat : Natural A B coe𝟙 + nat = nat' - fromEq : NaturalTransformation A B - fromEq = coe𝟙 , nat + fromEq : NaturalTransformation A B + fromEq = coe𝟙 , nat module _ {A B : Functor ℂ 𝔻} where obverse : A ≡ B → A ≅ B diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index e7e2024..f5af047 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -328,6 +328,8 @@ module _ {ℓ : Level} where SetsHasProducts = record { product = product } module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where + open Category ℂ + -- Covariant Presheaf Representable : Set (ℓa ⊔ lsuc ℓb) Representable = Functor ℂ (𝓢𝓮𝓽 ℓb) @@ -336,8 +338,6 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where Presheaf : Set (ℓa ⊔ lsuc ℓb) Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb) - open Category ℂ - -- The "co-yoneda" embedding. representable : Category.Object ℂ → Representable representable A = record diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index d00a3ec..9447023 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -28,9 +28,12 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where private 𝓢 = Sets ℓ open Fun (opposite ℂ) 𝓢 - presheaf = Cat.Categories.Sets.presheaf ℂ + module ℂ = Category ℂ + presheaf : ℂ.Object → Presheaf ℂ + presheaf = Cat.Categories.Sets.presheaf ℂ + module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where fmap : Transformation (presheaf A) (presheaf B) fmap C x = ℂ [ f ∘ x ] From 71d9acff9a96fb65c5205e3ea7c7d19139da3b56 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 20 Mar 2018 17:27:41 +0100 Subject: [PATCH 20/38] Stuff about half-time report --- proposal/BACKLOG.md | 22 ++++++ proposal/halftime.tex | 177 ++++++++++++++++++++++++++++++++++++++++++ proposal/macros.tex | 6 ++ proposal/proposal.tex | 3 + 4 files changed, 208 insertions(+) create mode 100644 proposal/BACKLOG.md create mode 100644 proposal/halftime.tex diff --git a/proposal/BACKLOG.md b/proposal/BACKLOG.md new file mode 100644 index 0000000..b889c92 --- /dev/null +++ b/proposal/BACKLOG.md @@ -0,0 +1,22 @@ +Remove stuff about models of type theory + +Add references to specific (noteable) implementaitons of category theory: +* Unimath +* cubicaltt +* https://github.com/pcapriotti/agda-categories +* https://github.com/copumpkin/categories +* ... + +Talk about structure of library: +=== + +Propositional- and non-propositional stuff split up +Providing "equiality principles" +Provide overview of what has been proven. + +What can I say about reusability? + +Misc +==== + +Propositional content diff --git a/proposal/halftime.tex b/proposal/halftime.tex new file mode 100644 index 0000000..11dc836 --- /dev/null +++ b/proposal/halftime.tex @@ -0,0 +1,177 @@ +\section{Halftime report} +I've written this as an appendix because 1) the aim of the thesis changed +drastically from the planning report/proposal 2) partly I'm not sure how to +structure my thesis. + +My work so far has very much focused on the formalization, i.e. coding. It's +unclear to me at this point what I should have in the final report. Here I will +describe what I have managed to formalize so far and what outstanding challenges +I'm facing. + +\subsection{Implementation overview} +The overall structure of my project is as follows: + +\begin{itemize} +\item Core categorical concepts +\subitem Categories +\subitem Functors +\subitem Products +\subitem Exponentials +\subitem Cartesian closed categories +\subitem Natural transformations +\subitem Yoneda embedding +\subitem Monads +\subsubitem Monoidal monads +\subsubitem Kleisli monads +\subsubitem Voevodsky's construction +\item Category of \ldots +\subitem Homotopy sets +\subitem Categories +\subitem Relations +\subitem Functors +\subitem Free category +\end{itemize} + +I also started work on the category with families as well as the cubical +category as per the original goal of the thesis. However I have not gotten so +far with this. + +In the following I will give an overview of overall results in each of these +categories (no pun). + +As an overall design-guideline I've defined concepts in a such a way that the +``data'' and the ``laws'' about that data is split up in seperate modules. As an +example a category is defined to have two members: `raw` which is a collection +of the data and `isCategory` which asserts some laws about that data. + +This allows me to reason about things in a more mathematical way, where one can +reason about two categories by simply focusing on the data. This is acheived by +creating a function embodying the ``equality principle'' for a given record. In +the case of monads, to prove two categories propositionally equal it enough to +provide a proof that their data is equal. + +\subsubsection{Categories} +Defines the basic notion of a category. This definition closely follows that of +[HoTT]: That is, the standard definition of a category (data; objects, arrows, +composition and identity, laws; preservation of identity and composition) plus +the extra condition that it is univalent - namely that you can get an equality +of two objects from an isomorphism. + +I make no distinction between a pre-category and a real category (as in the +[HoTT]-sense). A pre-category in my implementation would be a category sans the +witness to univalence. + +I also prove that being a category is a proposition. This gives rise to an +equality principle for monads that focuses on the data-part. + +I also show that the opposite category is indeed a category. (\WIP{} I have not +shown that univalence holds for such a construction) + +I also show that taking the opposite is an involution. + +\subsubsection{Functors} +Defines the notion of a functor - also split up into data and laws. + +Propositionality for being a functor. + +Composition of functors and the identity functor. + +\subsubsection{Products} +Definition of what it means for an object to be a product in a given category. + +Definition of what it means for a category to have all products. + +\WIP Prove propositionality for being a product and having products. + +\subsubsection{Exponentials} +Definition of what it means to be an exponential object. + +Definition of what it means for a category to have all exponential objects. + +\subsubsection{Cartesian closed categories} +Definition of what it means for a category to be cartesian closed; namely that +it has all products and all exponentials. + +\subsubsection{Natural transformations} +Definition of transformations\footnote{Maybe this is a name I made up for a + family of morphisms} and the naturality condition for these. + +Proof that naturality is a mere proposition and the accompanying equality +principle. Proof that natural transformations are homotopic sets. + +The identity natural transformation. + +\subsubsection{Yoneda embedding} + +The yoneda embedding is typically presented in terms of the category of +categories (cf. Awodey) \emph however this is not stricly needed - all we need +is what would be the exponential object in that category - this happens to be +functors and so this is how we define the yoneda embedding. + +\subsubsection{Monads} + +Defines an equivalence between these two formulations of a monad: + +\subsubsubsection{Monoidal monads} + +Defines the standard monoidal representation of a monad: + +An endofunctor with two natural transformations (called ``pure'' and ``join'') +and some laws about these natural transformations. + +Propositionality proofs and equality principle is provided. + +\subsubsubsection{Kleisli monads} + +A presentation of monads perhaps more familiar to a functional programer: + +A map on objects and two maps on morphisms (called ``pure'' and ``bind'') and +some laws about these maps. + +Propositionality proofs and equality principle is provided. + +\subsubsubsection{Voevodsky's construction} + +Provides construction 2.3 as presented in an unpublished paper by the late +Vladimir Voevodsky. This construction is similiar to the equivalence provided +for the two preceding formulations +\footnote{ TODO: I would like to include in the thesis some motivation for why + this construction is particularly interesting.} + +\subsubsection{Homotopy sets} +The typical category of sets where the objects are modelled by an Agda set +(henceforth ``type'') at a given level is not a valid category in this cubical +settings, we need to restrict the types to be those that are homotopy sets. Thus the objects of this category are: +% +$$\Set_\ell \defeq \sum_{A \tp \MCU_\ell} \isSet\ A$$ +% +\WIP{} I'm still missing a few details for the proof that this category is +univalent. Indeed this doesn't not follow immediately from +% +$$\mathit{univalence} \tp (A \cong B) \simeq (A \simeq B)$$ +% +since $A$ and $B$ are of type $\MCU \neq \Set$. +\subsubsection{Categories} +Note that this category does in fact not exist. In stead I provide the +definition of the ``raw'' category as well as some of the laws. + +Furthermore I provide some helpful lemmas about this raw category. For instance +I have shown what would be the exponential object in such a category. + +These lemmas can be used to provide the actual exponential object in a context +where we have a witness to this being a category. This is useful if this library +is later extended to talk about higher categories. + +\subsubsection{Functors} +The category of functors and natural transformations. An immediate corrolary is +the set of presheaf categories. + +\WIP{} I have not shown that the category of functors is univalent. + +\subsubsection{Relations} +The category of relations. \WIP I have not shown that this category is +univalent. Not sure I intend to do so either. + +\subsubsection{Free category} +The free category of a category. \WIP I have not shown that this category is +univalent. diff --git a/proposal/macros.tex b/proposal/macros.tex index d1bf101..2653ac3 100644 --- a/proposal/macros.tex +++ b/proposal/macros.tex @@ -18,3 +18,9 @@ \newcommand{\fmap}{\mathit{fmap}} \newcommand{\idFun}{\mathit{id}} \newcommand{\Sets}{\mathit{Sets}} +\newcommand{\Set}{\mathit{Set}} +\newcommand{\MCU}{\UU} +\newcommand{\isSet}{\mathit{isSet}} +\newcommand{\tp}{\;\mathord{:}\;} +\newcommand{\subsubsubsection}[1]{\textbf{#1}} +\newcommand{\WIP}[1]{\textbf{[WIP]}} diff --git a/proposal/proposal.tex b/proposal/proposal.tex index c6cb67d..073ecb5 100644 --- a/proposal/proposal.tex +++ b/proposal/proposal.tex @@ -13,6 +13,8 @@ \usepackage{multicol} \usepackage{amsmath,amssymb} \usepackage[toc,page]{appendix} +\usepackage{xspace} + % \setlength{\parskip}{10pt} % \usepackage{tikz} @@ -282,5 +284,6 @@ The thesis shall conclude with a discussion about the benefits of Cubical Agda. \bibliography{refs} \begin{appendices} \input{planning.tex} +\input{halftime.tex} \end{appendices} \end{document} From 4beb48e066b813166d2ab31c3c4da60e72940488 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 11:46:36 +0100 Subject: [PATCH 21/38] Use correct order for left- and right identity Define and use helpers left- and right identity --- src/Cat/Categories/Cat.agda | 8 ++-- src/Cat/Categories/Free.agda | 2 +- src/Cat/Categories/Fun.agda | 10 ++--- src/Cat/Categories/Rel.agda | 8 ++-- src/Cat/Categories/Sets.agda | 44 ++++++++++----------- src/Cat/Category.agda | 24 +++++++---- src/Cat/Category/Monad.agda | 8 ++-- src/Cat/Category/Monad/Kleisli.agda | 12 +++--- src/Cat/Category/Monad/Monoidal.agda | 4 +- src/Cat/Category/NaturalTransformation.agda | 4 +- src/Cat/Category/Yoneda.agda | 2 +- 11 files changed, 65 insertions(+), 61 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index f429985..9038605 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -47,7 +47,7 @@ module _ (ℓ ℓ' : Level) where isAssociative : IsAssociative isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H} ident : IsIdentity identity - ident = ident-r , ident-l + ident = ident-l , ident-r -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- however, form a groupoid! Therefore there is no (1-)category of @@ -241,10 +241,10 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where ident : fmap {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 ident = begin - fmap {c} {c} (𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩ - fmap {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ + fmap {c} {c} (𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩ + fmap {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ 𝔻 [ identityTrans F C ∘ F.fmap (𝟙 ℂ)] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F.fmap (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩ + 𝔻 [ 𝟙 𝔻 ∘ F.fmap (𝟙 ℂ)] ≡⟨ 𝔻.leftIdentity ⟩ F.fmap (𝟙 ℂ) ≡⟨ F.isIdentity ⟩ 𝟙 𝔻 ∎ where diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index 9d8d3d4..bda3820 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -55,7 +55,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ident-l = refl isIdentity : IsIdentity 𝟙 - isIdentity = ident-r , ident-l + isIdentity = ident-l , ident-r open Univalence isIdentity diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 9bbb438..14bbdd2 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -45,18 +45,18 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C eq-r : ∀ C → (𝔻 [ f' C ∘ identityTrans A C ]) ≡ f' C eq-r C = begin 𝔻 [ f' C ∘ identityTrans A C ] ≡⟨⟩ - 𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ proj₁ 𝔻.isIdentity ⟩ + 𝔻 [ f' C ∘ 𝔻.𝟙 ] ≡⟨ 𝔻.rightIdentity ⟩ f' C ∎ eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C - eq-l C = proj₂ 𝔻.isIdentity + eq-l C = 𝔻.leftIdentity ident-r : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f ident-r = lemSig allNatural _ _ (funExt eq-r) ident-l : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f ident-l = lemSig allNatural _ _ (funExt eq-l) isIdentity - : (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f - × (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f - isIdentity = ident-r , ident-l + : (NT[_∘_] {A} {B} {B} (NT.identity B) f) ≡ f + × (NT[_∘_] {A} {A} {B} f (NT.identity A)) ≡ f + isIdentity = ident-l , ident-r -- Functor categories. Objects are functors, arrows are natural transformations. RawFun : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd') RawFun = record diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 1dbed3d..ac645ef 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -76,9 +76,9 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where ≃ (a , b) ∈ S equi = backwards Cubical.FromStdLib., isequiv - ident-l : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) + ident-r : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ≡ (a , b) ∈ S - ident-l = equivToPath equi + ident-r = equivToPath equi module _ where private @@ -110,9 +110,9 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where ≃ ab ∈ S equi = backwards Cubical.FromStdLib., isequiv - ident-r : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) + ident-l : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ≡ ab ∈ S - ident-r = equivToPath equi + ident-l = equivToPath equi module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset (C × D)} (ad : A × D) where private diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index f5af047..ce94104 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -287,39 +287,35 @@ module _ {ℓ : Level} where open Category 𝓢 open import Cubical.Sigma - module _ (0A 0B : Object) where + module _ (hA hB : Object) where + open Σ hA renaming (proj₁ to A ; proj₂ to sA) + open Σ hB renaming (proj₁ to B ; proj₂ to sB) + private - A : Set ℓ - A = proj₁ 0A - sA : isSet A - sA = proj₂ 0A - B : Set ℓ - B = proj₁ 0B - sB : isSet B - sB = proj₂ 0B - 0A×0B : Object - 0A×0B = (A × B) , sigPresSet sA λ _ → sB + productObject : Object + productObject = (A × B) , sigPresSet sA λ _ → sB module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where _&&&_ : (X → A × B) _&&&_ x = f x , g x - module _ {0X : Object} where - X = proj₁ 0X - module _ (f : X → A ) (g : X → B) where - lem : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g - proj₁ lem = refl - proj₂ lem = refl - rawProduct : RawProduct 𝓢 0A 0B - RawProduct.object rawProduct = 0A×0B + module _ (hX : Object) where + open Σ hX renaming (proj₁ to X) + module _ (f : X → A ) (g : X → B) where + ump : proj₁ Function.∘′ (f &&& g) ≡ f × proj₂ Function.∘′ (f &&& g) ≡ g + proj₁ ump = refl + proj₂ ump = refl + + rawProduct : RawProduct 𝓢 hA hB + RawProduct.object rawProduct = productObject RawProduct.proj₁ rawProduct = Data.Product.proj₁ RawProduct.proj₂ rawProduct = Data.Product.proj₂ isProduct : IsProduct 𝓢 _ _ rawProduct - IsProduct.ump isProduct {X = X} f g - = (f &&& g) , lem {0X = X} f g + IsProduct.ump isProduct {X = hX} f g + = (f &&& g) , ump hX f g - product : Product 𝓢 0A 0B + product : Product 𝓢 hA hB Product.raw product = rawProduct Product.isProduct product = isProduct @@ -346,7 +342,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ; fmap = ℂ [_∘_] } ; isFunctor = record - { isIdentity = funExt λ _ → proj₂ isIdentity + { isIdentity = funExt λ _ → leftIdentity ; isDistributive = funExt λ x → sym isAssociative } } @@ -359,7 +355,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where ; fmap = λ f g → ℂ [ g ∘ f ] } ; isFunctor = record - { isIdentity = funExt λ x → proj₁ isIdentity + { isIdentity = funExt λ x → rightIdentity ; isDistributive = funExt λ x → isAssociative } } diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 834ff47..370da37 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -96,7 +96,7 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where IsIdentity : ({A : Object} → Arrow A A) → Set (ℓa ⊔ ℓb) IsIdentity id = {A B : Object} {f : Arrow A B} - → f ∘ id ≡ f × id ∘ f ≡ f + → id ∘ f ≡ f × f ∘ id ≡ f ArrowsAreSets : Set (ℓa ⊔ ℓb) ArrowsAreSets = ∀ {A B : Object} → isSet (Arrow A B) @@ -166,29 +166,37 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc field univalent : Univalent + leftIdentity : {A B : Object} {f : Arrow A B} → 𝟙 ∘ f ≡ f + leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) + -- leftIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) + + rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ 𝟙 ≡ f + rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) + -- rightIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) + -- Some common lemmas about categories. module _ {A B : Object} {X : Object} (f : Arrow A B) where iso-is-epi : Isomorphism f → Epimorphism {X = X} f iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin - g₀ ≡⟨ sym (fst isIdentity) ⟩ + g₀ ≡⟨ sym rightIdentity ⟩ g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩ (g₀ ∘ f) ∘ f- ≡⟨ cong (λ φ → φ ∘ f-) eq ⟩ (g₁ ∘ f) ∘ f- ≡⟨ sym isAssociative ⟩ g₁ ∘ (f ∘ f-) ≡⟨ cong (_∘_ g₁) right-inv ⟩ - g₁ ∘ 𝟙 ≡⟨ fst isIdentity ⟩ + g₁ ∘ 𝟙 ≡⟨ rightIdentity ⟩ g₁ ∎ iso-is-mono : Isomorphism f → Monomorphism {X = X} f iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq = begin - g₀ ≡⟨ sym (snd isIdentity) ⟩ + g₀ ≡⟨ sym leftIdentity ⟩ 𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ (f- ∘ f) ∘ g₀ ≡⟨ sym isAssociative ⟩ f- ∘ (f ∘ g₀) ≡⟨ cong (_∘_ f-) eq ⟩ f- ∘ (f ∘ g₁) ≡⟨ isAssociative ⟩ (f- ∘ f) ∘ g₁ ≡⟨ cong (λ φ → φ ∘ g₁) left-inv ⟩ - 𝟙 ∘ g₁ ≡⟨ snd isIdentity ⟩ + 𝟙 ∘ g₁ ≡⟨ leftIdentity ⟩ g₁ ∎ iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f @@ -201,7 +209,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where open RawCategory ℂ module _ (ℂ : IsCategory ℂ) where - open IsCategory ℂ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent) + open IsCategory ℂ using (isAssociative ; arrowsAreSets ; Univalent ; leftIdentity ; rightIdentity) open import Cubical.NType open import Cubical.NType.Properties @@ -233,11 +241,11 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where open Cubical.NType.Properties geq : g ≡ g' geq = begin - g ≡⟨ sym (fst isIdentity) ⟩ + g ≡⟨ sym rightIdentity ⟩ g ∘ 𝟙 ≡⟨ cong (λ φ → g ∘ φ) (sym ε') ⟩ g ∘ (f ∘ g') ≡⟨ isAssociative ⟩ (g ∘ f) ∘ g' ≡⟨ cong (λ φ → φ ∘ g') η ⟩ - 𝟙 ∘ g' ≡⟨ snd isIdentity ⟩ + 𝟙 ∘ g' ≡⟨ leftIdentity ⟩ g' ∎ propUnivalent : isProp Univalent diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index 3eef523..f6cb1a9 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -124,7 +124,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where bind (f >>> (pure >>> bind 𝟙)) ≡⟨ cong (λ φ → bind (f >>> φ)) (isNatural _) ⟩ bind (f >>> 𝟙) - ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + ≡⟨ cong bind ℂ.leftIdentity ⟩ bind f ∎ forthRawEq : forthRaw (backRaw m) ≡ K.Monad.raw m @@ -155,7 +155,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where KM.bind 𝟙 ≡⟨⟩ bind 𝟙 ≡⟨⟩ joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → _ ∘ φ) R.isIdentity ⟩ - joinT X ∘ 𝟙 ≡⟨ proj₁ ℂ.isIdentity ⟩ + joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩ joinT X ∎ fmapEq : ∀ {A B} → KM.fmap {A} {B} ≡ Rfmap @@ -167,7 +167,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where Rfmap (f >>> pureT B) >>> joinT B ≡⟨ cong (λ φ → φ >>> joinT B) R.isDistributive ⟩ Rfmap f >>> Rfmap (pureT B) >>> joinT B ≡⟨ ℂ.isAssociative ⟩ joinT B ∘ Rfmap (pureT B) ∘ Rfmap f ≡⟨ cong (λ φ → φ ∘ Rfmap f) (proj₂ isInverse) ⟩ - 𝟙 ∘ Rfmap f ≡⟨ proj₂ ℂ.isIdentity ⟩ + 𝟙 ∘ Rfmap f ≡⟨ ℂ.leftIdentity ⟩ Rfmap f ∎ ) @@ -192,7 +192,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where M.RawMonad.joinT (backRaw (forth m)) X ≡⟨⟩ KM.join ≡⟨⟩ joinT X ∘ Rfmap 𝟙 ≡⟨ cong (λ φ → joinT X ∘ φ) R.isIdentity ⟩ - joinT X ∘ 𝟙 ≡⟨ proj₁ ℂ.isIdentity ⟩ + joinT X ∘ 𝟙 ≡⟨ ℂ.rightIdentity ⟩ joinT X ∎) joinNTEq : (λ i → NaturalTransformation F[ Req i ∘ Req i ] (Req i)) diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda index 8f96b82..eedbeb7 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -104,7 +104,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where isFunctorR : IsFunctor ℂ ℂ rawR IsFunctor.isIdentity isFunctorR = begin - bind (pure ∘ 𝟙) ≡⟨ cong bind (proj₁ ℂ.isIdentity) ⟩ + bind (pure ∘ 𝟙) ≡⟨ cong bind (ℂ.rightIdentity) ⟩ bind pure ≡⟨ isIdentity ⟩ 𝟙 ∎ @@ -156,9 +156,9 @@ record IsMonad (raw : RawMonad) : Set ℓ where bind (bind (f >>> pure) >>> (pure >>> bind 𝟙)) ≡⟨ cong (λ φ → bind (bind (f >>> pure) >>> φ)) (isNatural _) ⟩ bind (bind (f >>> pure) >>> 𝟙) - ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + ≡⟨ cong bind ℂ.leftIdentity ⟩ bind (bind (f >>> pure)) - ≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩ + ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩ bind (𝟙 >>> bind (f >>> pure)) ≡⟨⟩ bind (𝟙 >=> (f >>> pure)) ≡⟨ sym (isDistributive _ _) ⟩ @@ -186,10 +186,10 @@ record IsMonad (raw : RawMonad) : Set ℓ where bind (join >>> (pure >>> bind 𝟙)) ≡⟨ cong (λ φ → bind (join >>> φ)) (isNatural _) ⟩ bind (join >>> 𝟙) - ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + ≡⟨ cong bind ℂ.leftIdentity ⟩ bind join ≡⟨⟩ bind (bind 𝟙) - ≡⟨ cong bind (sym (proj₁ ℂ.isIdentity)) ⟩ + ≡⟨ cong bind (sym ℂ.rightIdentity) ⟩ bind (𝟙 >>> bind 𝟙) ≡⟨⟩ bind (𝟙 >=> 𝟙) ≡⟨ sym (isDistributive _ _) ⟩ bind 𝟙 >>> bind 𝟙 ≡⟨⟩ @@ -212,7 +212,7 @@ record IsMonad (raw : RawMonad) : Set ℓ where bind (pure >>> (pure >>> bind 𝟙)) ≡⟨ cong (λ φ → bind (pure >>> φ)) (isNatural _) ⟩ bind (pure >>> 𝟙) - ≡⟨ cong bind (proj₂ ℂ.isIdentity) ⟩ + ≡⟨ cong bind ℂ.leftIdentity ⟩ bind pure ≡⟨ isIdentity ⟩ 𝟙 ∎ diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index b969187..52cfc5e 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -75,8 +75,8 @@ record IsMonad (raw : RawMonad) : Set ℓ where joinT Y ∘ (R.fmap f ∘ pureT X) ≡⟨ cong (λ φ → joinT Y ∘ φ) (sym (pureN f)) ⟩ joinT Y ∘ (pureT (R.omap Y) ∘ f) ≡⟨ ℂ.isAssociative ⟩ joinT Y ∘ pureT (R.omap Y) ∘ f ≡⟨ cong (λ φ → φ ∘ f) (proj₁ isInverse) ⟩ - 𝟙 ∘ f ≡⟨ proj₂ ℂ.isIdentity ⟩ - f ∎ + 𝟙 ∘ f ≡⟨ ℂ.leftIdentity ⟩ + f ∎ isDistributive : IsDistributive isDistributive {X} {Y} {Z} g f = sym aux diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index 2ccef94..82ef983 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -72,8 +72,8 @@ module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level} identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F) identityNatural F {A = A} {B = B} f = begin 𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩ - F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩ + 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ 𝔻.leftIdentity ⟩ + F→ f ≡⟨ sym 𝔻.rightIdentity ⟩ 𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩ 𝔻 [ F→ f ∘ identityTrans F A ] ∎ where diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index 9447023..7a1a0bc 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -54,7 +54,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where isIdentity {c} = lemSig (naturalIsProp {F = presheaf c} {presheaf c}) _ _ eq where eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (presheaf c) - eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity + eq = funExt λ A → funExt λ B → ℂ.leftIdentity isDistributive : IsDistributive isDistributive {A} {B} {C} {f = f} {g} From e98ed89db576d4c3fe26dfe86b9d72f0bb925109 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 12:17:10 +0100 Subject: [PATCH 22/38] Make propositionality a submodule of the actual proposition --- src/Cat/Category.agda | 47 ++++++++++++++++------------------- src/Cat/Category/Product.agda | 2 +- 2 files changed, 22 insertions(+), 27 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 370da37..0db82c2 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -36,9 +36,11 @@ open import Data.Product renaming ; ∃! to ∃!≈ ) open import Data.Empty -import Function +import Function + open import Cubical -open import Cubical.NType.Properties using ( propIsEquiv ; lemPropF ) +open import Cubical.NType +open import Cubical.NType.Properties open import Cat.Wishlist @@ -168,11 +170,9 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc leftIdentity : {A B : Object} {f : Arrow A B} → 𝟙 ∘ f ≡ f leftIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) - -- leftIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ 𝟙 ≡ f rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) - -- rightIdentity {A} {B} {f} = fst (isIdentity {A = A} {B} {f}) -- Some common lemmas about categories. module _ {A B : Object} {X : Object} (f : Arrow A B) where @@ -188,7 +188,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc g₁ ∎ iso-is-mono : Isomorphism f → Monomorphism {X = X} f - iso-is-mono (f- , (left-inv , right-inv)) g₀ g₁ eq = + iso-is-mono (f- , left-inv , right-inv) g₀ g₁ eq = begin g₀ ≡⟨ sym leftIdentity ⟩ 𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ @@ -202,17 +202,8 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso --- | Propositionality of being a category --- --- Proves that all projections of `IsCategory` are mere propositions as well as --- `IsCategory` itself being a mere proposition. -module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where - open RawCategory ℂ - module _ (ℂ : IsCategory ℂ) where - open IsCategory ℂ using (isAssociative ; arrowsAreSets ; Univalent ; leftIdentity ; rightIdentity) - open import Cubical.NType - open import Cubical.NType.Properties - + -- | All projections are propositions. + module Propositionality where propIsAssociative : isProp IsAssociative propIsAssociative x y i = arrowsAreSets _ _ x y i @@ -251,18 +242,22 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where propUnivalent : isProp Univalent propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i +-- | Propositionality of being a category +module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where + open RawCategory ℂ + open Univalence private module _ (x y : IsCategory ℂ) where - module IC = IsCategory module X = IsCategory x module Y = IsCategory y - open Univalence -- In a few places I use the result of propositionality of the various - -- projections of `IsCategory` - I've arbitrarily chosed to use this + -- projections of `IsCategory` - Here I arbitrarily chose to use this -- result from `x : IsCategory C`. I don't know which (if any) possibly -- adverse effects this may have. + module Prop = X.Propositionality + isIdentity : (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ Y.isIdentity ] - isIdentity = propIsIdentity x X.isIdentity Y.isIdentity + isIdentity = Prop.propIsIdentity X.isIdentity Y.isIdentity U : ∀ {a : IsIdentity 𝟙} → (λ _ → IsIdentity 𝟙) [ X.isIdentity ≡ a ] → (b : Univalent a) @@ -275,16 +270,16 @@ module Propositionality {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where P y eq = ∀ (univ : Univalent y) → U eq univ p : ∀ (b' : Univalent X.isIdentity) → (λ _ → Univalent X.isIdentity) [ X.univalent ≡ b' ] - p univ = propUnivalent x X.univalent univ + p univ = Prop.propUnivalent X.univalent univ helper : P Y.isIdentity isIdentity helper = pathJ P p Y.isIdentity isIdentity eqUni : U isIdentity Y.univalent 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 + IsCategory.isAssociative (done i) = Prop.propIsAssociative X.isAssociative Y.isAssociative i + IsCategory.isIdentity (done i) = isIdentity i + IsCategory.arrowsAreSets (done i) = Prop.propArrowIsSet X.arrowsAreSets Y.arrowsAreSets i + IsCategory.univalent (done i) = eqUni i propIsCategory : isProp (IsCategory ℂ) propIsCategory = done @@ -309,7 +304,7 @@ module _ {ℓa ℓb : Level} {ℂ 𝔻 : Category ℓa ℓb} where module _ (rawEq : ℂ.raw ≡ 𝔻.raw) where private isCategoryEq : (λ i → IsCategory (rawEq i)) [ ℂ.isCategory ≡ 𝔻.isCategory ] - isCategoryEq = lemPropF Propositionality.propIsCategory rawEq + isCategoryEq = lemPropF propIsCategory rawEq Category≡ : ℂ ≡ 𝔻 Category≡ i = record diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 1ddeed9..c459566 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -7,7 +7,7 @@ open import Cubical.NType.Properties using (lemPropF) open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂) -open import Cat.Category hiding (module Propositionality) +open import Cat.Category module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where From 890154a81d6829bd9081b1a8467511021016881c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 12:28:26 +0100 Subject: [PATCH 23/38] Simplify qualified imports, change make-target: clean --- Makefile | 2 +- src/Cat/Categories/Sets.agda | 16 +++++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile index f2e26be..1a3e6e8 100644 --- a/Makefile +++ b/Makefile @@ -2,4 +2,4 @@ build: src/**.agda agda src/Cat.agda clean: - rm src/**/*.agdai + find src -name "*.agdai" -type f -delete diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index ce94104..f109b0c 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -16,9 +16,11 @@ open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product open import Cat.Wishlist -open import Cat.Equivalence as Eqv renaming (module NoEta to Eeq) using (AreInverses ; module Equiv≃) +open import Cat.Equivalence as Eqv using (AreInverses ; module Equiv≃ ; module NoEta) -module Equivalence = Eeq.Equivalence′ +open NoEta + +module Equivalence = Equivalence′ _⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C eqA ⊙ eqB = Equivalence.compose eqA eqB @@ -122,7 +124,7 @@ module _ (ℓ : Level) where module _ {ℓa ℓb : Level} {A : Set ℓa} {P : A → Set ℓb} where lem2 : ((x : A) → isProp (P x)) → (p q : Σ A P) → (p ≡ q) ≃ (proj₁ p ≡ proj₁ q) - lem2 pA p q = Eeq.fromIsomorphism iso + lem2 pA p q = fromIsomorphism iso where f : p ≡ q → proj₁ p ≡ proj₁ q f e i = proj₁ (e i) @@ -186,7 +188,7 @@ module _ (ℓ : Level) where iso : Σ A P Eqv.≅ Σ A Q iso = f , g , inv res : Σ A P ≃ Σ A Q - res = Eeq.fromIsomorphism iso + res = fromIsomorphism iso module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where lem4 : isSet A → isSet B → (f : A → B) @@ -207,7 +209,7 @@ module _ (ℓ : Level) where { verso-recto = funExt re-ve ; recto-verso = funExt ve-re } - in Eeq.fromIsomorphism iso + in fromIsomorphism iso module _ {hA hB : Object} where private @@ -240,7 +242,7 @@ module _ (ℓ : Level) where eqv : Σ (A → B) (isEquiv A B) Eqv.≅ (A ≃ B) eqv = obv , inv , areInv hh : Σ (A → B) (isEquiv A B) ≃ (A ≃ B) - hh = Eeq.fromIsomorphism eqv + hh = fromIsomorphism eqv -- lem2 with propIsSet step2 : (A ≡ B) ≃ (hA ≡ hB) @@ -248,7 +250,7 @@ module _ (ℓ : Level) where -- Go from an isomorphism on sets to an isomorphism on homotopic sets trivial? : (hA ≅ hB) ≃ Σ (A → B) isIso - trivial? = sym≃ (Eeq.fromIsomorphism res) + trivial? = sym≃ (fromIsomorphism res) where fwd : Σ (A → B) isIso → hA ≅ hB fwd (f , g , inv) = f , g , inv.toPair From ed3b3047e6cba45e6f09180c2d51e7e6a6f68191 Mon Sep 17 00:00:00 2001 From: Andrea Vezzosi Date: Wed, 21 Mar 2018 12:00:47 +0000 Subject: [PATCH 24/38] Progress on univalence for sets. --- src/Cat/Categories/Sets.agda | 22 +++++++--------------- 1 file changed, 7 insertions(+), 15 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 0c7f420..07ba934 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -123,24 +123,16 @@ module _ (ℓ : Level) where → (p ≡ q) ≃ (proj₁ p ≡ proj₁ q) lem2 pA p q = Eeq.fromIsomorphism iso where - f : p ≡ q → proj₁ p ≡ proj₁ q + f : ∀ {p q} → p ≡ q → proj₁ p ≡ proj₁ q f e i = proj₁ (e i) - g : proj₁ p ≡ proj₁ q → p ≡ q - g = lemSig pA p q + g : ∀ {p q} → proj₁ p ≡ proj₁ q → p ≡ q + g {p} {q} = lemSig pA p q ve-re : (e : p ≡ q) → (g ∘ f) e ≡ e - -- QUESTION Why does `h` not satisfy the constraint here? - ve-re e i j = qq0 j , {!h!} - where - -- qq : ? [ proj₂ ((g ∘ f) e) ≡ proj₂ e ] - qq0 : proj₁ p ≡ proj₁ q - qq0 i = proj₁ (e i) - qq : (λ i → P (qq0 i)) [ proj₂ p ≡ proj₂ q ] - qq = lemPropF pA qq0 - h : P (qq0 j) - h = qq j - re-ve : (e : proj₁ p ≡ proj₁ q) → (f ∘ g) e ≡ e + ve-re = pathJ (\ q (e : p ≡ q) → (g ∘ f) e ≡ e) + (\ i j → p .proj₁ , propSet (pA (p .proj₁)) (p .proj₂) (p .proj₂) (λ i → (g {p} {p} ∘ f) (λ i₁ → p) i .proj₂) (λ i → p .proj₂) i j ) q + re-ve : (e : proj₁ p ≡ proj₁ q) → (f {p} {q} ∘ g {p} {q}) e ≡ e re-ve e = refl - inv : AreInverses f g + inv : AreInverses (f {p} {q}) (g {p} {q}) inv = record { verso-recto = funExt ve-re ; recto-verso = funExt re-ve From cd3514c8cf1d4dc86d30272f67c819e27fb5129e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 13:25:24 +0100 Subject: [PATCH 25/38] Formatting --- src/Cat/Categories/Cat.agda | 155 ++++++++++++++---------------------- 1 file changed, 59 insertions(+), 96 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 9038605..1be64e0 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -18,8 +18,6 @@ open import Cat.Category.NaturalTransformation open import Cat.Equality open Equality.Data.Product -open Category using (Object ; 𝟙) - -- The category of categories module _ (ℓ ℓ' : Level) where private @@ -35,19 +33,18 @@ module _ (ℓ ℓ' : Level) where ident-l = Functor≡ refl RawCat : RawCategory (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') - RawCat = - record - { Object = Category ℓ ℓ' - ; Arrow = Functor - ; 𝟙 = identity - ; _∘_ = F[_∘_] - } + RawCategory.Object RawCat = Category ℓ ℓ' + RawCategory.Arrow RawCat = Functor + RawCategory.𝟙 RawCat = identity + RawCategory._∘_ RawCat = F[_∘_] + private open RawCategory RawCat isAssociative : IsAssociative isAssociative {f = F} {G} {H} = assc {F = F} {G = G} {H = H} - ident : IsIdentity identity - ident = ident-l , ident-r + + isIdentity : IsIdentity identity + isIdentity = ident-l , ident-r -- NB! `ArrowsAreSets RawCat` is *not* provable. The type of functors, -- however, form a groupoid! Therefore there is no (1-)category of @@ -55,7 +52,7 @@ module _ (ℓ ℓ' : Level) where -- -- Because of this there is no category of categories. Cat : (unprovable : IsCategory RawCat) → Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') - Category.raw (Cat _) = RawCat + Category.raw (Cat _) = RawCat Category.isCategory (Cat unprovable) = unprovable -- | In the following we will pretend there is a category of categories when @@ -72,28 +69,31 @@ module CatProduct {ℓ ℓ' : Level} (ℂ 𝔻 : Category ℓ ℓ') where module ℂ = Category ℂ module 𝔻 = Category 𝔻 - Obj = Object ℂ × Object 𝔻 - Arr : Obj → Obj → Set ℓ' - Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] - 𝟙' : {o : Obj} → Arr o o - 𝟙' = 𝟙 ℂ , 𝟙 𝔻 - _∘_ : - {a b c : Obj} → - Arr b c → - Arr a b → - Arr a c - _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} + module _ where + private + Obj = ℂ.Object × 𝔻.Object + Arr : Obj → Obj → Set ℓ' + Arr (c , d) (c' , d') = ℂ [ c , c' ] × 𝔻 [ d , d' ] + 𝟙 : {o : Obj} → Arr o o + 𝟙 = ℂ.𝟙 , 𝔻.𝟙 + _∘_ : + {a b c : Obj} → + Arr b c → + Arr a b → + Arr a c + _∘_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → ℂ [ bc∈C ∘ ab∈C ] , 𝔻 [ bc∈D ∘ ab∈D ]} - rawProduct : RawCategory ℓ ℓ' - RawCategory.Object rawProduct = Obj - RawCategory.Arrow rawProduct = Arr - RawCategory.𝟙 rawProduct = 𝟙' - RawCategory._∘_ rawProduct = _∘_ - open RawCategory rawProduct + rawProduct : RawCategory ℓ ℓ' + RawCategory.Object rawProduct = Obj + RawCategory.Arrow rawProduct = Arr + RawCategory.𝟙 rawProduct = 𝟙 + RawCategory._∘_ rawProduct = _∘_ + + open RawCategory rawProduct arrowsAreSets : ArrowsAreSets arrowsAreSets = setSig {sA = ℂ.arrowsAreSets} {sB = λ x → 𝔻.arrowsAreSets} - isIdentity : IsIdentity 𝟙' + isIdentity : IsIdentity 𝟙 isIdentity = Σ≡ (fst ℂ.isIdentity) (fst 𝔻.isIdentity) , Σ≡ (snd ℂ.isIdentity) (snd 𝔻.isIdentity) @@ -189,102 +189,65 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where Categoryℓ = Category ℓ ℓ open Fun ℂ 𝔻 renaming (identity to idN) - omap : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 + omap : Functor ℂ 𝔻 × ℂ.Object → 𝔻.Object omap (F , A) = Functor.omap F A -- The exponential object object : Categoryℓ object = Fun - module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where + module _ {dom cod : Functor ℂ 𝔻 × ℂ.Object} where + open Σ dom renaming (proj₁ to F ; proj₂ to A) + open Σ cod renaming (proj₁ to G ; proj₂ to B) private - F : Functor ℂ 𝔻 - F = proj₁ dom - A : Object ℂ - A = proj₂ dom - - G : Functor ℂ 𝔻 - G = proj₁ cod - B : Object ℂ - B = proj₂ cod - module F = Functor F module G = Functor G fmap : (pobj : NaturalTransformation F G × ℂ [ A , B ]) → 𝔻 [ F.omap A , G.omap B ] - fmap ((θ , θNat) , f) = result - where - θA : 𝔻 [ F.omap A , G.omap A ] - θA = θ A - θB : 𝔻 [ F.omap B , G.omap B ] - θB = θ B - F→f : 𝔻 [ F.omap A , F.omap B ] - F→f = F.fmap f - G→f : 𝔻 [ G.omap A , G.omap B ] - G→f = G.fmap f - l : 𝔻 [ F.omap A , G.omap B ] - l = 𝔻 [ θB ∘ F.fmap f ] - r : 𝔻 [ F.omap A , G.omap B ] - r = 𝔻 [ G.fmap f ∘ θA ] - result : 𝔻 [ F.omap A , G.omap B ] - result = l + fmap ((θ , θNat) , f) = 𝔻 [ θ B ∘ F.fmap f ] + -- Alternatively: + -- + -- fmap ((θ , θNat) , f) = 𝔻 [ G.fmap f ∘ θ A ] + -- + -- Since they are equal by naturality of θ. open CatProduct renaming (object to _⊗_) using () - module _ {c : Functor ℂ 𝔻 × Object ℂ} where - private - F : Functor ℂ 𝔻 - F = proj₁ c - C : Object ℂ - C = proj₂ c + module _ {c : Functor ℂ 𝔻 × ℂ.Object} where + open Σ c renaming (proj₁ to F ; proj₂ to C) - ident : fmap {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 + ident : fmap {c} {c} (NT.identity F , ℂ.𝟙 {A = proj₂ c}) ≡ 𝔻.𝟙 ident = begin - fmap {c} {c} (𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩ - fmap {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ - 𝔻 [ identityTrans F C ∘ F.fmap (𝟙 ℂ)] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F.fmap (𝟙 ℂ)] ≡⟨ 𝔻.leftIdentity ⟩ - F.fmap (𝟙 ℂ) ≡⟨ F.isIdentity ⟩ - 𝟙 𝔻 ∎ + fmap {c} {c} (Category.𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩ + fmap {c} {c} (idN F , ℂ.𝟙) ≡⟨⟩ + 𝔻 [ identityTrans F C ∘ F.fmap ℂ.𝟙 ] ≡⟨⟩ + 𝔻 [ 𝔻.𝟙 ∘ F.fmap ℂ.𝟙 ] ≡⟨ 𝔻.leftIdentity ⟩ + F.fmap ℂ.𝟙 ≡⟨ F.isIdentity ⟩ + 𝔻.𝟙 ∎ where module F = Functor F - module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where + module _ {F×A G×B H×C : Functor ℂ 𝔻 × ℂ.Object} where + open Σ F×A renaming (proj₁ to F ; proj₂ to A) + open Σ G×B renaming (proj₁ to G ; proj₂ to B) + open Σ H×C renaming (proj₁ to H ; proj₂ to C) private - F = F×A .proj₁ - A = F×A .proj₂ - G = G×B .proj₁ - B = G×B .proj₂ - H = H×C .proj₁ - C = H×C .proj₂ module F = Functor F module G = Functor G module H = Functor H module _ - -- NaturalTransformation F G × ℂ .Arrow A B {θ×f : NaturalTransformation F G × ℂ [ A , B ]} {η×g : NaturalTransformation G H × ℂ [ B , C ]} where + open Σ θ×f renaming (proj₁ to θNT ; proj₂ to f) + open Σ θNT renaming (proj₁ to θ ; proj₂ to θNat) + open Σ η×g renaming (proj₁ to ηNT ; proj₂ to g) + open Σ ηNT renaming (proj₁ to η ; proj₂ to ηNat) private - θ : Transformation F G - θ = proj₁ (proj₁ θ×f) - θNat : Natural F G θ - θNat = proj₂ (proj₁ θ×f) - f : ℂ [ A , B ] - f = proj₂ θ×f - η : Transformation G H - η = proj₁ (proj₁ η×g) - ηNat : Natural G H η - ηNat = proj₂ (proj₁ η×g) - g : ℂ [ B , C ] - g = proj₂ η×g - ηθNT : NaturalTransformation F H - ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat) - - ηθ = proj₁ ηθNT - ηθNat = proj₂ ηθNT + ηθNT = NT[_∘_] {F} {G} {H} ηNT θNT + open Σ ηθNT renaming (proj₁ to ηθ ; proj₂ to ηθNat) isDistributive : 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ F.fmap ( ℂ [ g ∘ f ] ) ] From 183906dc8c59d8bae268b385bac9c04939fe99da Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 14:39:56 +0100 Subject: [PATCH 26/38] Define and use custom prelude --- src/Cat/Categories/Cat.agda | 8 +++---- src/Cat/Categories/Sets.agda | 40 ++++++++++++++++++++++++++----- src/Cat/Category.agda | 35 +++++++-------------------- src/Cat/Category/Exponential.agda | 4 +--- src/Cat/Category/Product.agda | 7 ++---- src/Cat/Prelude.agda | 40 +++++++++++++++++++++++++++++++ 6 files changed, 89 insertions(+), 45 deletions(-) create mode 100644 src/Cat/Prelude.agda diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 1be64e0..2e28452 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -3,8 +3,7 @@ module Cat.Categories.Cat where -open import Agda.Primitive -open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) +open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd) open import Cubical open import Cubical.Sigma @@ -14,6 +13,7 @@ open import Cat.Category.Functor open import Cat.Category.Product open import Cat.Category.Exponential hiding (_×_ ; product) open import Cat.Category.NaturalTransformation +open import Cat.Categories.Fun open import Cat.Equality open Equality.Data.Product @@ -182,8 +182,6 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where -- it is therefory also cartesian closed. module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where private - open Data.Product - open import Cat.Categories.Fun module ℂ = Category ℂ module 𝔻 = Category 𝔻 Categoryℓ = Category ℓ ℓ @@ -217,7 +215,7 @@ module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where module _ {c : Functor ℂ 𝔻 × ℂ.Object} where open Σ c renaming (proj₁ to F ; proj₂ to C) - ident : fmap {c} {c} (NT.identity F , ℂ.𝟙 {A = proj₂ c}) ≡ 𝔻.𝟙 + ident : fmap {c} {c} (NT.identity F , ℂ.𝟙 {A = snd c}) ≡ 𝔻.𝟙 ident = begin fmap {c} {c} (Category.𝟙 (object ⊗ ℂ) {c}) ≡⟨⟩ fmap {c} {c} (idN F , ℂ.𝟙) ≡⟨⟩ diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 98da7b1..52db3a5 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -2,15 +2,13 @@ {-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Categories.Sets where -open import Agda.Primitive -open import Data.Product +open import Cat.Prelude hiding (_≃_) +import Data.Product + open import Function using (_∘_) --- open import Cubical using (funExt ; refl ; isSet ; isProp ; _≡_ ; isEquiv ; sym ; trans ; _[_≡_] ; I ; Path ; PathP) open import Cubical hiding (_≃_) open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua) -open import Cubical.GradLemma -open import Cubical.NType.Properties open import Cat.Category open import Cat.Category.Functor @@ -260,9 +258,39 @@ module _ (ℓ : Level) where -- `(id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)` ? res : isEquiv (hA ≡ hB) (hA ≅ hB) (_≃_.eqv t) res = _≃_.isEqv t + thr : (hA ≡ hB) ≃ (hA ≅ hB) + thr = con _ res + -- p : _ → (hX : Object) → Path (hA ≅ hB) (hA ≡ hB) + -- p = ? + -- p hA X i0 = hA ~ X + -- p hA X i1 = Path Obj hA X + + -- From Thierry: + -- + -- -Any- equality proof of + -- + -- Id (Obj C) c0 c1 + -- + -- and + -- + -- iso c0 c1 + -- + -- is enough to ensure univalence. + -- This is because this implies that + -- + -- Sigma (x : Obj C) is c0 x + -- + -- is contractible, which implies univalence. + + univalent' : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) + univalent' hA = {!!} , {!!} + module _ {hA hB : hSet {ℓ}} where + + -- Thierry: `thr0` implies univalence. univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) - univalent = let k = _≃_.isEqv (sym≃ conclusion) in {!k!} + univalent = univalent'→univalent univalent' + -- let k = _≃_.isEqv (sym≃ conclusion) in {! k!} SetsIsCategory : IsCategory SetsRaw IsCategory.isAssociative SetsIsCategory = refl diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 0db82c2..74e4262 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -28,36 +28,14 @@ module Cat.Category where -open import Agda.Primitive -open import Data.Unit.Base -open import Data.Product renaming +open import Cat.Prelude + renaming ( proj₁ to fst ; proj₂ to snd - ; ∃! to ∃!≈ ) -open import Data.Empty + import Function -open import Cubical -open import Cubical.NType -open import Cubical.NType.Properties - -open import Cat.Wishlist - ------------------ --- * Utilities -- ------------------ - --- | Unique existensials. -∃! : ∀ {a b} {A : Set a} - → (A → Set b) → Set (a ⊔ b) -∃! = ∃!≈ _≡_ - -∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b) -∃!-syntax = ∃ - -syntax ∃!-syntax (λ x → B) = ∃![ x ] B - ----------------- -- * Categories -- ----------------- @@ -148,6 +126,12 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where -- ∀ A → isContr (Σ[ X ∈ Object ] iso A X) -- future work ideas: compile to CAM + Univalent' : Set _ + Univalent' = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) + + module _ (univalent' : Univalent') where + univalent'→univalent : Univalent + univalent'→univalent = {!!} -- | The mere proposition of being a category. -- @@ -229,7 +213,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc isoIsProp a@(g , η , ε) a'@(g' , η' , ε') = lemSig (λ g → propIsInverseOf) a a' geq where - open Cubical.NType.Properties geq : g ≡ g' geq = begin g ≡⟨ sym rightIdentity ⟩ diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda index 87769f6..76652d2 100644 --- a/src/Cat/Category/Exponential.agda +++ b/src/Cat/Category/Exponential.agda @@ -1,8 +1,6 @@ module Cat.Category.Exponential where -open import Agda.Primitive -open import Data.Product hiding (_×_) -open import Cubical +open import Cat.Prelude hiding (_×_) open import Cat.Category open import Cat.Category.Product diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index c459566..1ce45c5 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -1,11 +1,8 @@ {-# OPTIONS --allow-unsolved-metas #-} module Cat.Category.Product where -open import Agda.Primitive -open import Cubical -open import Cubical.NType.Properties using (lemPropF) - -open import Data.Product as P hiding (_×_ ; proj₁ ; proj₂) +open import Cat.Prelude hiding (_×_ ; proj₁ ; proj₂) +import Data.Product as P open import Cat.Category diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda new file mode 100644 index 0000000..0a047d9 --- /dev/null +++ b/src/Cat/Prelude.agda @@ -0,0 +1,40 @@ +-- | Custom prelude for this module +module Cat.Prelude where + +open import Agda.Primitive public +-- FIXME Use: +-- open import Agda.Builtin.Sigma public +-- Rather than +open import Data.Product public + renaming (∃! to ∃!≈) + +-- TODO Import Data.Function under appropriate names. + +open import Cubical public +-- FIXME rename `gradLemma` to `fromIsomorphism` - perhaps just use wrapper +-- module. +open import Cubical.GradLemma + using (gradLemma) + public +open import Cubical.NType + using (⟨-2⟩) + public +open import Cubical.NType.Properties + using + ( lemPropF ; lemSig ; lemSigP ; isSetIsProp + ; propPi ; propHasLevel ; setPi ; propSet) + public + +----------------- +-- * Utilities -- +----------------- + +-- | Unique existensials. +∃! : ∀ {a b} {A : Set a} + → (A → Set b) → Set (a ⊔ b) +∃! = ∃!≈ _≡_ + +∃!-syntax : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b) +∃!-syntax = ∃ + +syntax ∃!-syntax (λ x → B) = ∃![ x ] B From 29f45d1426ed6b83357e1259d126c0f8831c72ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 14:47:01 +0100 Subject: [PATCH 27/38] Delete equality module --- src/Cat/Categories/Cat.agda | 6 ------ src/Cat/Categories/Cube.agda | 5 +---- src/Cat/Categories/Fam.agda | 9 +-------- src/Cat/Category/Yoneda.agda | 6 +----- src/Cat/Equality.agda | 22 ---------------------- src/Cat/Prelude.agda | 10 ++++++++++ 6 files changed, 13 insertions(+), 45 deletions(-) delete mode 100644 src/Cat/Equality.agda diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 2e28452..e8a6f73 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -5,9 +5,6 @@ module Cat.Categories.Cat where open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd) -open import Cubical -open import Cubical.Sigma - open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product @@ -15,9 +12,6 @@ open import Cat.Category.Exponential hiding (_×_ ; product) open import Cat.Category.NaturalTransformation open import Cat.Categories.Fun -open import Cat.Equality -open Equality.Data.Product - -- The category of categories module _ (ℓ ℓ' : Level) where private diff --git a/src/Cat/Categories/Cube.agda b/src/Cat/Categories/Cube.agda index 00f10e3..f338343 100644 --- a/src/Cat/Categories/Cube.agda +++ b/src/Cat/Categories/Cube.agda @@ -1,21 +1,18 @@ {-# OPTIONS --allow-unsolved-metas #-} module Cat.Categories.Cube where +open import Cat.Prelude open import Level open import Data.Bool hiding (T) open import Data.Sum hiding ([_,_]) open import Data.Unit open import Data.Empty -open import Data.Product -open import Cubical open import Function open import Relation.Nullary open import Relation.Nullary.Decidable open import Cat.Category open import Cat.Category.Functor -open import Cat.Equality -open Equality.Data.Product -- See chapter 1 for a discussion on how presheaf categories are CwF's. diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index d100b77..6829a3b 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -1,17 +1,10 @@ {-# OPTIONS --allow-unsolved-metas #-} module Cat.Categories.Fam where -open import Agda.Primitive -open import Data.Product +open import Cat.Prelude import Function -open import Cubical -open import Cubical.Universe - open import Cat.Category -open import Cat.Equality - -open Equality.Data.Product module _ (ℓa ℓb : Level) where private diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index 7a1a0bc..47ac1ec 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -2,14 +2,10 @@ module Cat.Category.Yoneda where -open import Agda.Primitive -open import Data.Product -open import Cubical -open import Cubical.NType.Properties +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor -open import Cat.Equality open import Cat.Categories.Fun open import Cat.Categories.Sets hiding (presheaf) diff --git a/src/Cat/Equality.agda b/src/Cat/Equality.agda deleted file mode 100644 index d6b3dc0..0000000 --- a/src/Cat/Equality.agda +++ /dev/null @@ -1,22 +0,0 @@ -{-# OPTIONS --cubical #-} --- Defines equality-principles for data-types from the standard library. - -module Cat.Equality where - -open import Level -open import Cubical - --- _[_≡_] = PathP - -module Equality where - module Data where - module Product where - open import Data.Product - - module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B} - (proj₁≡ : (λ _ → A) [ proj₁ a ≡ proj₁ b ]) - (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where - - Σ≡ : a ≡ b - proj₁ (Σ≡ i) = proj₁≡ i - proj₂ (Σ≡ i) = proj₂≡ i diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index 0a047d9..0c2f523 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -24,6 +24,8 @@ open import Cubical.NType.Properties ( lemPropF ; lemSig ; lemSigP ; isSetIsProp ; propPi ; propHasLevel ; setPi ; propSet) public +open import Cubical.Sigma using (setSig) public +open import Cubical.Universe using (hSet) public ----------------- -- * Utilities -- @@ -38,3 +40,11 @@ open import Cubical.NType.Properties ∃!-syntax = ∃ syntax ∃!-syntax (λ x → B) = ∃![ x ] B + +module _ {ℓa ℓb : Level} {A : Set ℓa} {B : A → Set ℓb} {a b : Σ A B} + (proj₁≡ : (λ _ → A) [ proj₁ a ≡ proj₁ b ]) + (proj₂≡ : (λ i → B (proj₁≡ i)) [ proj₂ a ≡ proj₂ b ]) where + + Σ≡ : a ≡ b + proj₁ (Σ≡ i) = proj₁≡ i + proj₂ (Σ≡ i) = proj₂≡ i From ae0ff092f844ae1927e5a6e43dcd4d80c1f63931 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 14:56:43 +0100 Subject: [PATCH 28/38] Use prelude everywhere --- src/Cat/Categories/CwF.agda | 19 ++++++++----------- src/Cat/Categories/Free.agda | 8 +++----- src/Cat/Categories/Fun.agda | 8 +------- src/Cat/Categories/Rel.agda | 12 ++++-------- src/Cat/Categories/Sets.agda | 1 - src/Cat/Category/Monad.agda | 9 +-------- src/Cat/Category/Monad/Kleisli.agda | 6 +----- src/Cat/Category/Monad/Monoidal.agda | 6 +----- src/Cat/Category/Monad/Voevodsky.agda | 10 ++-------- src/Cat/Category/NaturalTransformation.agda | 9 +++------ src/Cat/Prelude.agda | 2 +- 11 files changed, 25 insertions(+), 65 deletions(-) diff --git a/src/Cat/Categories/CwF.agda b/src/Cat/Categories/CwF.agda index ea369ef..45dbf2b 100644 --- a/src/Cat/Categories/CwF.agda +++ b/src/Cat/Categories/CwF.agda @@ -1,36 +1,33 @@ module Cat.Categories.CwF where -open import Agda.Primitive -open import Data.Product +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor open import Cat.Categories.Fam -open Category -open Functor - module _ {ℓa ℓb : Level} where record CwF : Set (lsuc (ℓa ⊔ ℓb)) where -- "A category with families consists of" field -- "A base category" ℂ : Category ℓa ℓb + module ℂ = Category ℂ -- It's objects are called contexts - Contexts = Object ℂ + Contexts = ℂ.Object -- It's arrows are called substitutions - Substitutions = Arrow ℂ + Substitutions = ℂ.Arrow field -- A functor T T : Functor (opposite ℂ) (Fam ℓa ℓb) -- Empty context - [] : Terminal ℂ + [] : ℂ.Terminal private module T = Functor T - Type : (Γ : Object ℂ) → Set ℓa + Type : (Γ : ℂ.Object) → Set ℓa Type Γ = proj₁ (proj₁ (T.omap Γ)) - module _ {Γ : Object ℂ} {A : Type Γ} where + module _ {Γ : ℂ.Object} {A : Type Γ} where -- module _ {A B : Object ℂ} {γ : ℂ [ A , B ]} where -- k : Σ (proj₁ (omap T B) → proj₁ (omap T A)) @@ -46,7 +43,7 @@ module _ {ℓa ℓb : Level} where record ContextComprehension : Set (ℓa ⊔ ℓb) where field - Γ&A : Object ℂ + Γ&A : ℂ.Object proj1 : ℂ [ Γ&A , Γ ] -- proj2 : ???? diff --git a/src/Cat/Categories/Free.agda b/src/Cat/Categories/Free.agda index bda3820..1d262dd 100644 --- a/src/Cat/Categories/Free.agda +++ b/src/Cat/Categories/Free.agda @@ -1,11 +1,9 @@ {-# OPTIONS --allow-unsolved-metas #-} module Cat.Categories.Free where -open import Agda.Primitive -open import Relation.Binary +open import Cat.Prelude hiding (Path ; empty) -open import Cubical hiding (Path ; empty) -open import Data.Product +open import Relation.Binary open import Cat.Category @@ -60,7 +58,7 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where open Univalence isIdentity module _ {A B : ℂ.Object} where - arrowsAreSets : Cubical.isSet (Path ℂ.Arrow A B) + arrowsAreSets : isSet (Path ℂ.Arrow A B) arrowsAreSets a b p q = {!!} eqv : isEquiv (A ≡ B) (A ≅ B) (Univalence.id-to-iso isIdentity A B) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 14bbdd2..18165d3 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -1,13 +1,7 @@ {-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Categories.Fun where -open import Agda.Primitive -open import Data.Product - - -open import Cubical -open import Cubical.GradLemma -open import Cubical.NType.Properties +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor hiding (identity) diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index ac645ef..5b44601 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -1,12 +1,8 @@ {-# OPTIONS --cubical --allow-unsolved-metas #-} module Cat.Categories.Rel where -open import Cubical -open import Cubical.GradLemma -open import Agda.Primitive -open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) +open import Cat.Prelude renaming (proj₁ to fst ; proj₂ to snd) open import Function -import Cubical.FromStdLib open import Cat.Category @@ -74,7 +70,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where equi : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ≃ (a , b) ∈ S - equi = backwards Cubical.FromStdLib., isequiv + equi = backwards , isequiv ident-r : (Σ[ a' ∈ A ] (a , a') ∈ Diag A × (a' , b) ∈ S) ≡ (a , b) ∈ S @@ -108,7 +104,7 @@ module _ {A B : Set} {S : Subset (A × B)} (ab : A × B) where equi : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ≃ ab ∈ S - equi = backwards Cubical.FromStdLib., isequiv + equi = backwards , isequiv ident-l : (Σ[ b' ∈ B ] (a , b') ∈ S × (b' , b) ∈ Diag B) ≡ ab ∈ S @@ -146,7 +142,7 @@ module _ {A B C D : Set} {S : Subset (A × B)} {R : Subset (B × C)} {Q : Subset equi : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) ≃ (Σ[ b ∈ B ] (a , b) ∈ S × (Σ[ c ∈ C ] (b , c) ∈ R × (c , d) ∈ Q)) - equi = fwd Cubical.FromStdLib., isequiv + equi = fwd , isequiv -- isAssociativec : Q + (R + S) ≡ (Q + R) + S is-isAssociative : (Σ[ c ∈ C ] (Σ[ b ∈ B ] (a , b) ∈ S × (b , c) ∈ R) × (c , d) ∈ Q) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 52db3a5..a54cba1 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -7,7 +7,6 @@ import Data.Product open import Function using (_∘_) -open import Cubical hiding (_≃_) open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua) open import Cat.Category diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda index f6cb1a9..3b65149 100644 --- a/src/Cat/Category/Monad.agda +++ b/src/Cat/Category/Monad.agda @@ -20,14 +20,7 @@ The monoidal representation is exposed by default from this module. {-# OPTIONS --cubical --allow-unsolved-metas #-} module Cat.Category.Monad where -open import Agda.Primitive - -open import Data.Product - -open import Cubical -open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) -open import Cubical.GradLemma using (gradLemma) - +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor as F open import Cat.Category.NaturalTransformation diff --git a/src/Cat/Category/Monad/Kleisli.agda b/src/Cat/Category/Monad/Kleisli.agda index eedbeb7..7377cdf 100644 --- a/src/Cat/Category/Monad/Kleisli.agda +++ b/src/Cat/Category/Monad/Kleisli.agda @@ -4,11 +4,7 @@ The Kleisli formulation of monads {-# OPTIONS --cubical --allow-unsolved-metas #-} open import Agda.Primitive -open import Data.Product - -open import Cubical -open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) -open import Cubical.GradLemma using (gradLemma) +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor as F diff --git a/src/Cat/Category/Monad/Monoidal.agda b/src/Cat/Category/Monad/Monoidal.agda index 52cfc5e..360e5df 100644 --- a/src/Cat/Category/Monad/Monoidal.agda +++ b/src/Cat/Category/Monad/Monoidal.agda @@ -4,11 +4,7 @@ Monoidal formulation of monads {-# OPTIONS --cubical --allow-unsolved-metas #-} open import Agda.Primitive -open import Data.Product - -open import Cubical -open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) -open import Cubical.GradLemma using (gradLemma) +open import Cat.Prelude open import Cat.Category open import Cat.Category.Functor as F diff --git a/src/Cat/Category/Monad/Voevodsky.agda b/src/Cat/Category/Monad/Voevodsky.agda index 5f27ed0..f30aa9a 100644 --- a/src/Cat/Category/Monad/Voevodsky.agda +++ b/src/Cat/Category/Monad/Voevodsky.agda @@ -4,14 +4,8 @@ This module provides construction 2.3 in [voe] {-# OPTIONS --cubical --allow-unsolved-metas --caching #-} module Cat.Category.Monad.Voevodsky where -open import Agda.Primitive - -open import Data.Product -open import Function using (_∘_ ; _$_) - -open import Cubical -open import Cubical.NType.Properties using (lemPropF ; lemSig ; lemSigP) -open import Cubical.GradLemma using (gradLemma) +open import Cat.Prelude +open import Function open import Cat.Category open import Cat.Category.Functor as F diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda index 82ef983..13e3d89 100644 --- a/src/Cat/Category/NaturalTransformation.agda +++ b/src/Cat/Category/NaturalTransformation.agda @@ -19,15 +19,12 @@ -- * A composition operator. {-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Category.NaturalTransformation where -open import Agda.Primitive -open import Data.Product + +open import Cat.Prelude + open import Data.Nat using (_≤_ ; z≤n ; s≤s) module Nat = Data.Nat -open import Cubical -open import Cubical.Sigma -open import Cubical.NType.Properties - open import Cat.Category open import Cat.Category.Functor hiding (identity) open import Cat.Wishlist diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index 0c2f523..d936e60 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -24,7 +24,7 @@ open import Cubical.NType.Properties ( lemPropF ; lemSig ; lemSigP ; isSetIsProp ; propPi ; propHasLevel ; setPi ; propSet) public -open import Cubical.Sigma using (setSig) public +open import Cubical.Sigma using (setSig ; sigPresSet) public open import Cubical.Universe using (hSet) public ----------------- From 8f67ff9f363779fef4a41969b45364682ede4dde Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 15:01:31 +0100 Subject: [PATCH 29/38] Use explicit parameter for hSet --- src/Cat/Categories/Sets.agda | 8 +++----- src/Cat/Prelude.agda | 15 +++++++++++++-- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index a54cba1..75ff8b0 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -59,10 +59,8 @@ module _ {ℓ : Level} {A B : Set ℓ} {a : A} where module _ (ℓ : Level) where private - open import Cubical.Universe using (hSet) public - SetsRaw : RawCategory (lsuc ℓ) ℓ - RawCategory.Object SetsRaw = hSet {ℓ} + RawCategory.Object SetsRaw = hSet ℓ RawCategory.Arrow SetsRaw (T , _) (U , _) = T → U RawCategory.𝟙 SetsRaw = Function.id RawCategory._∘_ SetsRaw = Function._∘′_ @@ -79,7 +77,7 @@ module _ (ℓ : Level) where arrowsAreSets {B = (_ , s)} = setPi λ _ → s isIso = Eqv.Isomorphism - module _ {hA hB : hSet {ℓ}} where + module _ {hA hB : hSet ℓ} where open Σ hA renaming (proj₁ to A ; proj₂ to sA) open Σ hB renaming (proj₁ to B ; proj₂ to sB) lem1 : (f : A → B) → isSet A → isSet B → isProp (isIso f) @@ -284,7 +282,7 @@ module _ (ℓ : Level) where univalent' : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) univalent' hA = {!!} , {!!} - module _ {hA hB : hSet {ℓ}} where + module _ {hA hB : hSet ℓ} where -- Thierry: `thr0` implies univalence. univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index d936e60..c17fda0 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -17,7 +17,7 @@ open import Cubical.GradLemma using (gradLemma) public open import Cubical.NType - using (⟨-2⟩) + using (⟨-2⟩ ; ⟨-1⟩ ; ⟨0⟩ ; TLevel ; HasLevel) public open import Cubical.NType.Properties using @@ -25,7 +25,18 @@ open import Cubical.NType.Properties ; propPi ; propHasLevel ; setPi ; propSet) public open import Cubical.Sigma using (setSig ; sigPresSet) public -open import Cubical.Universe using (hSet) public + +module _ (ℓ : Level) where + -- FIXME Ask if we can push upstream. + -- A redefinition of `Cubical.Universe` with an explicit parameter + _-type : TLevel → Set (lsuc ℓ) + n -type = Σ (Set ℓ) (HasLevel n) + + hSet : Set (lsuc ℓ) + hSet = ⟨0⟩ -type + + Prop : Set (lsuc ℓ) + Prop = ⟨-1⟩ -type ----------------- -- * Utilities -- From 181edc0cd589355dd5b494e57e107487547d11f6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 17:52:32 +0100 Subject: [PATCH 30/38] Prove step 3 in proof of unvivalence for hSet without `ua` --- src/Cat/Categories/Fam.agda | 2 +- src/Cat/Categories/Sets.agda | 49 +++++++++++++++++++++++------------ src/Cat/Category.agda | 38 +++++++++++++++++++-------- src/Cat/Category/Functor.agda | 9 +++---- 4 files changed, 65 insertions(+), 33 deletions(-) diff --git a/src/Cat/Categories/Fam.agda b/src/Cat/Categories/Fam.agda index 6829a3b..5ffde56 100644 --- a/src/Cat/Categories/Fam.agda +++ b/src/Cat/Categories/Fam.agda @@ -8,7 +8,7 @@ open import Cat.Category module _ (ℓa ℓb : Level) where private - Object = Σ[ hA ∈ hSet {ℓa} ] (proj₁ hA → hSet {ℓb}) + Object = Σ[ hA ∈ hSet ℓa ] (proj₁ hA → hSet ℓb) Arr : Object → Object → Set (ℓa ⊔ ℓb) Arr ((A , _) , B) ((A' , _) , B') = Σ[ f ∈ (A → A') ] ({x : A} → proj₁ (B x) → proj₁ (B' (f x))) 𝟙 : {A : Object} → Arr A A diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 75ff8b0..65533a4 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -147,26 +147,47 @@ module _ (ℓ : Level) where Q→P : ∀ {a} → Q a ≡ P a Q→P = sym P→Q f : Σ A P → Σ A Q - f (a , pA) = a , coe P→Q pA + f (a , pA) = a , _≃_.eqv (eA a) pA g : Σ A Q → Σ A P - g (a , qA) = a , coe Q→P qA + g (a , qA) = a , g' qA + where + module E = Equivalence (eA a) + k : Eqv.Isomorphism _ + k = E.toIso (_≃_.isEqv (eA a)) + open Σ k renaming (proj₁ to g') ve-re : (x : Σ A P) → (g ∘ f) x ≡ x ve-re x i = proj₁ x , eq i where eq : proj₂ ((g ∘ f) x) ≡ proj₂ x eq = begin proj₂ ((g ∘ f) x) ≡⟨⟩ - coe Q→P (proj₂ (f x)) ≡⟨⟩ - coe Q→P (coe P→Q (proj₂ x)) ≡⟨ inv-coe P→Q ⟩ - proj₂ x ∎ + proj₂ (g (f (a , pA))) ≡⟨⟩ + g' (_≃_.eqv (eA a) pA) ≡⟨ lem ⟩ + pA ∎ + where + open Σ x renaming (proj₁ to a ; proj₂ to pA) + module E = Equivalence (eA a) + k : Eqv.Isomorphism _ + k = E.toIso (_≃_.isEqv (eA a)) + open Σ k renaming (proj₁ to g' ; proj₂ 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 = proj₁ x , eq i where + open Σ x renaming (proj₁ to a ; proj₂ to qA) eq = begin proj₂ ((f ∘ g) x) ≡⟨⟩ - coe P→Q (coe Q→P (proj₂ x)) ≡⟨⟩ - coe P→Q (coe (sym P→Q) (proj₂ x)) ≡⟨ inv-coe' P→Q ⟩ - proj₂ x ∎ + _≃_.eqv (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩ + qA ∎ + where + module E = Equivalence (eA a) + k : Eqv.Isomorphism _ + k = E.toIso (_≃_.isEqv (eA a)) + open Σ k renaming (proj₁ to g' ; proj₂ to inv) + module A = AreInverses inv inv : AreInverses f g inv = record { verso-recto = funExt ve-re @@ -279,15 +300,11 @@ module _ (ℓ : Level) where -- -- is contractible, which implies univalence. - univalent' : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) - univalent' hA = {!!} , {!!} + univalent[Contr] : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) + univalent[Contr] hA = {!!} , {!!} - module _ {hA hB : hSet ℓ} where - - -- Thierry: `thr0` implies univalence. - univalent : isEquiv (hA ≡ hB) (hA ≅ hB) (Univalence.id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB) - univalent = univalent'→univalent univalent' - -- let k = _≃_.isEqv (sym≃ conclusion) in {! k!} + univalent : Univalent + univalent = from[Contr] univalent[Contr] SetsIsCategory : IsCategory SetsRaw IsCategory.isAssociative SetsIsCategory = refl diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 74e4262..cd8a9ec 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -120,18 +120,16 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓ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. + + -- | Equivalent formulation of univalence. + Univalent[Contr] : Set _ + Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) + + -- From: Thierry Coquand + -- Date: Wed, Mar 21, 2018 at 3:12 PM -- - -- ∀ A → isContr (Σ[ X ∈ Object ] iso A X) - - -- future work ideas: compile to CAM - Univalent' : Set _ - Univalent' = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) - - module _ (univalent' : Univalent') where - univalent'→univalent : Univalent - univalent'→univalent = {!!} + -- This is not so straight-forward so you can assume it + postulate from[Contr] : Univalent[Contr] → Univalent -- | The mere proposition of being a category. -- @@ -208,6 +206,24 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc hh = arrowsAreSets _ _ (snd x) (snd y) in h i , hh i + module _ {A B : Object} {p q : A ≅ B} where + open Σ p renaming (proj₁ to pf) + open Σ (snd p) renaming (proj₁ to pg ; proj₂ to pAreInv) + open Σ q renaming (proj₁ to qf) + open Σ (snd q) renaming (proj₁ to qg ; proj₂ to qAreInv) + module _ (a : pf ≡ qf) (b : pg ≡ qg) where + private + open import Cubical.Sigma + open import Cubical.NType.Properties + -- Problem: How do I apply lempPropF twice? + cc : (λ i → IsInverseOf (a i) pg) [ pAreInv ≡ _ ] + cc = lemPropF (λ x → propIsInverseOf {A} {B} {x}) a + c : (λ i → IsInverseOf (a i) (b i)) [ pAreInv ≡ qAreInv ] + c = lemPropF (λ x → propIsInverseOf {A} {B} {{!!}}) {!cc!} + + ≅-equality : p ≡ q + ≅-equality i = a i , b i , c i + module _ {A B : Object} {f : Arrow A B} where isoIsProp : isProp (Isomorphism f) isoIsProp a@(g , η , ε) a'@(g' , η' , ε') = diff --git a/src/Cat/Category/Functor.agda b/src/Cat/Category/Functor.agda index 44b560e..390d8bc 100644 --- a/src/Cat/Category/Functor.agda +++ b/src/Cat/Category/Functor.agda @@ -78,8 +78,8 @@ EndoFunctor : ∀ {ℓa ℓb} (ℂ : Category ℓa ℓb) → Set _ EndoFunctor ℂ = Functor ℂ ℂ module _ - {ℓa ℓb : Level} - {ℂ 𝔻 : Category ℓa ℓb} + {ℓc ℓc' ℓd ℓd' : Level} + {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} (F : RawFunctor ℂ 𝔻) where private @@ -96,8 +96,7 @@ module _ -- Alternate version of above where `F` is indexed by an interval module _ - {ℓa ℓb : Level} - {ℂ 𝔻 : Category ℓa ℓb} + {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} {F : I → RawFunctor ℂ 𝔻} where private @@ -109,7 +108,7 @@ module _ IsFunctorIsProp' isF0 isF1 = lemPropF {B = IsFunctor ℂ 𝔻} (\ F → propIsFunctor F) (\ i → F i) -module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where +module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where open Functor Functor≡ : {F G : Functor ℂ 𝔻} → Functor.raw F ≡ Functor.raw G From 807a0f3dcdd76c3db5dfff02f7689220af4580ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 21 Mar 2018 18:05:25 +0100 Subject: [PATCH 31/38] Slight readability improvement --- src/Cat/Categories/Sets.agda | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 65533a4..b96822b 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -151,9 +151,8 @@ module _ (ℓ : Level) where g : Σ A Q → Σ A P g (a , qA) = a , g' qA where - module E = Equivalence (eA a) k : Eqv.Isomorphism _ - k = E.toIso (_≃_.isEqv (eA a)) + k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a)) open Σ k renaming (proj₁ to g') ve-re : (x : Σ A P) → (g ∘ f) x ≡ x ve-re x i = proj₁ x , eq i @@ -166,9 +165,8 @@ module _ (ℓ : Level) where pA ∎ where open Σ x renaming (proj₁ to a ; proj₂ to pA) - module E = Equivalence (eA a) k : Eqv.Isomorphism _ - k = E.toIso (_≃_.isEqv (eA a)) + k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a)) open Σ k renaming (proj₁ to g' ; proj₂ to inv) module A = AreInverses inv -- anti-funExt @@ -183,9 +181,8 @@ module _ (ℓ : Level) where _≃_.eqv (eA a) (g' qA) ≡⟨ (λ i → A.recto-verso i qA) ⟩ qA ∎ where - module E = Equivalence (eA a) k : Eqv.Isomorphism _ - k = E.toIso (_≃_.isEqv (eA a)) + k = Equiv≃.toIso _ _ (_≃_.isEqv (eA a)) open Σ k renaming (proj₁ to g' ; proj₂ to inv) module A = AreInverses inv inv : AreInverses f g From 66ab7138a63a643f5bc24ed845bc7249f7ee9822 Mon Sep 17 00:00:00 2001 From: Andrea Vezzosi Date: Thu, 22 Mar 2018 10:41:38 +0000 Subject: [PATCH 32/38] generalized lem3 and made progress for Sets univalence --- src/Cat/Categories/Sets.agda | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index b96822b..14be2a4 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -138,14 +138,10 @@ module _ (ℓ : Level) where iso : (p ≡ q) Eqv.≅ (proj₁ p ≡ proj₁ q) iso = f , g , inv - lem3 : {Q : A → Set ℓb} + lem3 : ∀ {ℓc} {Q : A → Set (ℓc ⊔ ℓb)} → ((a : A) → P a ≃ Q a) → Σ A P ≃ Σ A Q - lem3 {Q} eA = res + lem3 {Q = Q} eA = res where - P→Q : ∀ {a} → P a ≡ Q a - P→Q = ua (eA _) - Q→P : ∀ {a} → Q a ≡ P a - Q→P = sym P→Q f : Σ A P → Σ A Q f (a , pA) = a , _≃_.eqv (eA a) pA g : Σ A Q → Σ A P @@ -226,7 +222,7 @@ module _ (ℓ : Level) where -- lem3 and the equivalence from lem4 step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) - step0 = lem3 (λ f → sym≃ (lem4 sA sB f)) + step0 = lem3 {ℓc = lzero} (λ f → sym≃ (lem4 sA sB f)) -- univalence step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) step1 = hh ⊙ h @@ -297,8 +293,11 @@ module _ (ℓ : Level) where -- -- is contractible, which implies univalence. + eq1 : ∀ hA → (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB) + eq1 hA = (ua (lem3 (\ hB → sym≃ thr))) + univalent[Contr] : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) - univalent[Contr] hA = {!!} , {!!} + univalent[Contr] hA = subst {P = isContr} (sym (eq1 hA)) {!!} univalent : Univalent univalent = from[Contr] univalent[Contr] From d12122ce601eb423cb6c72bce5435552a93a1486 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 22 Mar 2018 11:50:07 +0100 Subject: [PATCH 33/38] Add another approach for univalence in Set --- src/Cat/Categories/Sets.agda | 59 +++++++++++++++++++++++++++++++----- src/Cat/Equivalence.agda | 10 ++++++ 2 files changed, 61 insertions(+), 8 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index b96822b..26e9ee7 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -1,11 +1,11 @@ -- | The category of homotopy sets -{-# OPTIONS --allow-unsolved-metas --cubical #-} +{-# OPTIONS --allow-unsolved-metas --cubical --caching #-} module Cat.Categories.Sets where open import Cat.Prelude hiding (_≃_) import Data.Product -open import Function using (_∘_) +open import Function using (_∘_ ; _∘′_) open import Cubical.Univalence using (univalence ; con ; _≃_ ; idtoeqv ; ua) @@ -267,12 +267,12 @@ module _ (ℓ : Level) where res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl } conclusion : (hA ≅ hB) ≃ (hA ≡ hB) conclusion = trivial? ⊙ step0 ⊙ step1 ⊙ step2 - t : (hA ≡ hB) ≃ (hA ≅ hB) - t = sym≃ conclusion + thierry : (hA ≡ hB) ≃ (hA ≅ hB) + thierry = sym≃ conclusion -- TODO Is the morphism `(_≃_.eqv conclusion)` the same as -- `(id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)` ? - res : isEquiv (hA ≡ hB) (hA ≅ hB) (_≃_.eqv t) - res = _≃_.isEqv t + res : isEquiv (hA ≡ hB) (hA ≅ hB) _ + res = _≃_.isEqv thierry thr : (hA ≡ hB) ≃ (hA ≅ hB) thr = con _ res -- p : _ → (hX : Object) → Path (hA ≅ hB) (hA ≡ hB) @@ -297,8 +297,51 @@ module _ (ℓ : Level) where -- -- is contractible, which implies univalence. - univalent[Contr] : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) - univalent[Contr] hA = {!!} , {!!} + module _ (hA : Object) where + open Σ hA renaming (proj₁ to A) + + center : Σ[ hB ∈ Object ] (hA ≅ hB) + center = hA , idIso hA + open Σ center renaming ({-proj₁ to hA ;-} proj₂ to isoA) using () + + module _ (y : Σ[ hC ∈ Object ] (hA ≅ hC)) where + open Σ y renaming (proj₁ to hC ; proj₂ to hA≅hC) + open Σ hC renaming (proj₁ to C) + + open Σ hA≅hC renaming (proj₁ to obv ; proj₂ to iso) + open Σ iso renaming (proj₁ to inv ; proj₂ to areInv) + + -- Idea: + -- Have : hA ≅ hC + -- Can I then construct `A Eqv.≅ C` + -- Cuz then it follows from univalence + A≡C : A ≡ C + A≡C = ua s + where + s0 : A Eqv.≅ C + s0 = obv , inv , Eqv.toAreInverses areInv + s : A ≃ C + s = fromIsomorphism s0 + + pObj : hA ≡ hC + pObj = lemSig (λ _ → isSetIsProp) hA hC A≡C + + abstract + isoEq + : (λ i → Σ (A → proj₁ (pObj i)) (Isomorphism {A = hA} {pObj i})) + [ idIso hA ≡ hA≅hC ] + isoEq = {!!} + where + d : ∀ iso → (λ _ → Σ (A → A) (Isomorphism {A = hA} {hA})) + [ idIso hA ≡ iso ] + d iso = {!!} + + isContractible : (hA , idIso hA) ≡ (hC , hA≅hC) + isContractible = Σ≡ pObj {!isoEq!} + -- isContractible = lemSig prop≅ center y pObj + + univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB) + univalent[Contr] = center , isContractible univalent : Univalent univalent = from[Contr] univalent[Contr] diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index c047330..fdbfc00 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -27,6 +27,16 @@ module _ {ℓa ℓb : Level} where Isomorphism : (f : A → B) → Set _ Isomorphism f = Σ (B → A) λ g → AreInverses f g + module _ {f : A → B} {g : B → A} + (inv : (g ∘ f) ≡ idFun A + × (f ∘ g) ≡ idFun B) where + open Σ inv renaming (fst to ve-re ; snd to re-ve) + toAreInverses : AreInverses f g + toAreInverses = record + { verso-recto = ve-re + ; recto-verso = re-ve + } + _≅_ : Set ℓa → Set ℓb → Set _ A ≅ B = Σ (A → B) Isomorphism From d816ba657b6ce963fad2d73059ec45136aa8e2a7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 22 Mar 2018 12:11:27 +0100 Subject: [PATCH 34/38] QED! Show that the category of homotopic sets are univalent. --- src/Cat/Categories/Sets.agda | 84 +++++------------------------------- 1 file changed, 11 insertions(+), 73 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 9266963..ad519bb 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -265,85 +265,23 @@ module _ (ℓ : Level) where conclusion = trivial? ⊙ step0 ⊙ step1 ⊙ step2 thierry : (hA ≡ hB) ≃ (hA ≅ hB) thierry = sym≃ conclusion - -- TODO Is the morphism `(_≃_.eqv conclusion)` the same as - -- `(id-to-iso (λ {A} {B} → isIdentity {A} {B}) hA hB)` ? - res : isEquiv (hA ≡ hB) (hA ≅ hB) _ - res = _≃_.isEqv thierry - thr : (hA ≡ hB) ≃ (hA ≅ hB) - thr = con _ res - -- p : _ → (hX : Object) → Path (hA ≅ hB) (hA ≡ hB) - -- p = ? - -- p hA X i0 = hA ~ X - -- p hA X i1 = Path Obj hA X - - -- From Thierry: - -- - -- -Any- equality proof of - -- - -- Id (Obj C) c0 c1 - -- - -- and - -- - -- iso c0 c1 - -- - -- is enough to ensure univalence. - -- This is because this implies that - -- - -- Sigma (x : Obj C) is c0 x - -- - -- is contractible, which implies univalence. module _ (hA : Object) where open Σ hA renaming (proj₁ to A) - center : Σ[ hB ∈ Object ] (hA ≅ hB) - center = hA , idIso hA - open Σ center renaming ({-proj₁ to hA ;-} proj₂ to isoA) using () + eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB) + eq1 = ua (lem3 (\ hB → sym≃ thierry)) - module _ (y : Σ[ hC ∈ Object ] (hA ≅ hC)) where - open Σ y renaming (proj₁ to hC ; proj₂ to hA≅hC) - open Σ hC renaming (proj₁ to C) + univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB) + univalent[Contr] = subst {P = isContr} (sym eq1) tres + where + module _ (y : Σ[ hB ∈ Object ] hA ≡ hB) where + open Σ y renaming (proj₁ to hB ; proj₂ to hA≡hB) + qres : (hA , refl) ≡ (hB , hA≡hB) + qres = contrSingl hA≡hB - open Σ hA≅hC renaming (proj₁ to obv ; proj₂ to iso) - open Σ iso renaming (proj₁ to inv ; proj₂ to areInv) - - -- Idea: - -- Have : hA ≅ hC - -- Can I then construct `A Eqv.≅ C` - -- Cuz then it follows from univalence - A≡C : A ≡ C - A≡C = ua s - where - s0 : A Eqv.≅ C - s0 = obv , inv , Eqv.toAreInverses areInv - s : A ≃ C - s = fromIsomorphism s0 - - pObj : hA ≡ hC - pObj = lemSig (λ _ → isSetIsProp) hA hC A≡C - - abstract - isoEq - : (λ i → Σ (A → proj₁ (pObj i)) (Isomorphism {A = hA} {pObj i})) - [ idIso hA ≡ hA≅hC ] - isoEq = {!!} - where - d : ∀ iso → (λ _ → Σ (A → A) (Isomorphism {A = hA} {hA})) - [ idIso hA ≡ iso ] - d iso = {!!} - - isContractible : (hA , idIso hA) ≡ (hC , hA≅hC) - isContractible = Σ≡ pObj {!isoEq!} - -- isContractible = lemSig prop≅ center y pObj - - -- univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB) - -- univalent[Contr] = center , isContractible - - eq1 : ∀ hA → (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB) - eq1 hA = ua (lem3 (\ hB → sym≃ thr)) - - univalent[Contr] : ∀ hA → isContr (Σ[ hB ∈ Object ] hA ≅ hB) - univalent[Contr] hA = subst {P = isContr} (sym (eq1 hA)) {!!} + tres : isContr (Σ[ hB ∈ Object ] hA ≡ hB) + tres = (hA , refl) , qres univalent : Univalent univalent = from[Contr] univalent[Contr] From 0246c1b5abf190ec08f6d0fb935dff4be6327e88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 22 Mar 2018 12:25:12 +0100 Subject: [PATCH 35/38] Readability --- src/Cat/Equivalence.agda | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index fdbfc00..f60deae 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -166,17 +166,13 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where toIso y ≡⟨ py ⟩ x ∎ where - helper : (x : Isomorphism _) → Σ _ λ y → toIso y ≡ x - helper (f~ , inv) = y , py - where - module inv = AreInverses inv - y : isEquiv _ _ f - y = {!!} - py : toIso y ≡ (f~ , inv) - py = {!!} - y : isEquiv _ _ _ - y = fst (helper x) - py = snd (helper x) + open Σ x renaming (fst to f~ ; snd to inv) + module inv = AreInverses inv + y : isEquiv _ _ f + y = {!!} + open Σ (toIso y) renaming (fst to f~' ; snd to inv') + py : toIso y ≡ (f~ , inv) + py = {!!} module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open Cubical.PathPrelude using (_≃_) From ebcab2528e9a7c3898a67e1bde277896261285cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 22 Mar 2018 13:49:53 +0100 Subject: [PATCH 36/38] Prove second inverse law for from/to-isomorphism --- src/Cat/Categories/Sets.agda | 10 ++--- src/Cat/Equivalence.agda | 71 ++++++++++++++++++++++++------------ 2 files changed, 51 insertions(+), 30 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index ad519bb..c18c39a 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -203,7 +203,7 @@ module _ (ℓ : Level) where re-ve : (x : isEquiv A B f) → (inv ∘ obv) x ≡ x re-ve = Equiv≃.inverse-from-to-iso A B ve-re : (x : isIso f) → (obv ∘ inv) x ≡ x - ve-re = Equiv≃.inverse-to-from-iso A B + ve-re = Equiv≃.inverse-to-from-iso A B sA sB iso : isEquiv A B f Eqv.≅ isIso f iso = obv , inv , record @@ -213,12 +213,8 @@ module _ (ℓ : Level) where in fromIsomorphism iso module _ {hA hB : Object} where - private - A = proj₁ hA - sA = proj₂ hA - B = proj₁ hB - sB = proj₂ hB - + open Σ hA renaming (proj₁ to A ; proj₂ to sA) + open Σ hB renaming (proj₁ to B ; proj₂ to sB) -- lem3 and the equivalence from lem4 step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) diff --git a/src/Cat/Equivalence.agda b/src/Cat/Equivalence.agda index f60deae..b63e4ec 100644 --- a/src/Cat/Equivalence.agda +++ b/src/Cat/Equivalence.agda @@ -75,15 +75,54 @@ module _ {ℓa ℓb ℓ : Level} (A : Set ℓa) (B : Set ℓb) where x ∎ -- `toIso` is abstract - so I probably can't close this proof. - -- inverse-to-from-iso : ∀ {f} → toIso {f} ∘ fromIso {f} ≡ idFun _ - -- inverse-to-from-iso = funExt (λ x → begin - -- (toIso ∘ fromIso) x ≡⟨⟩ - -- toIso (fromIso x) ≡⟨ cong toIso (propIsEquiv _ (fromIso x) y) ⟩ - -- toIso y ≡⟨ {!!} ⟩ - -- x ∎) - -- where - -- y : iseqv _ - -- y = {!!} + module _ (sA : isSet A) (sB : isSet B) where + module _ {f : A → B} (iso : Isomorphism f) where + module _ (iso-x iso-y : Isomorphism f) where + open Σ iso-x renaming (fst to x ; snd to inv-x) + open Σ iso-y renaming (fst to y ; snd to inv-y) + module inv-x = AreInverses inv-x + module inv-y = AreInverses inv-y + + fx≡fy : x ≡ y + fx≡fy = begin + x ≡⟨ cong (λ φ → x ∘ φ) (sym inv-y.recto-verso) ⟩ + x ∘ (f ∘ y) ≡⟨⟩ + (x ∘ f) ∘ y ≡⟨ cong (λ φ → φ ∘ y) inv-x.verso-recto ⟩ + y ∎ + + open import Cat.Prelude + + propInv : ∀ g → isProp (AreInverses f g) + propInv g t u i = record { verso-recto = a i ; recto-verso = b i } + where + module t = AreInverses t + module u = AreInverses u + a : t.verso-recto ≡ u.verso-recto + a i = h + where + hh : ∀ a → (g ∘ f) a ≡ a + hh a = sA ((g ∘ f) a) a (λ i → t.verso-recto i a) (λ i → u.verso-recto i a) i + h : g ∘ f ≡ idFun A + h i a = hh a i + b : t.recto-verso ≡ u.recto-verso + b i = h + where + hh : ∀ b → (f ∘ g) b ≡ b + hh b = sB _ _ (λ i → t.recto-verso i b) (λ i → u.recto-verso i b) i + h : f ∘ g ≡ idFun B + h i b = hh b i + + inx≡iny : (λ i → AreInverses f (fx≡fy i)) [ inv-x ≡ inv-y ] + inx≡iny = lemPropF propInv fx≡fy + + propIso : iso-x ≡ iso-y + propIso i = fx≡fy i , inx≡iny i + + inverse-to-from-iso : (toIso {f} ∘ fromIso {f}) iso ≡ iso + inverse-to-from-iso = begin + (toIso ∘ fromIso) iso ≡⟨⟩ + toIso (fromIso iso) ≡⟨ propIso _ _ ⟩ + iso ∎ fromIsomorphism : A ≅ B → A ~ B fromIsomorphism (f , iso) = f , fromIso iso @@ -159,20 +198,6 @@ module _ {ℓa ℓb : Level} (A : Set ℓa) (B : Set ℓb) where module Equiv≃ where open Equiv ≃isEquiv public - inverse-to-from-iso : ∀ {f} (x : _) → (toIso {f} ∘ fromIso {f}) x ≡ x - inverse-to-from-iso {f} x = begin - (toIso ∘ fromIso) x ≡⟨⟩ - toIso (fromIso x) ≡⟨ cong toIso (propIsEquiv _ (fromIso x) y) ⟩ - toIso y ≡⟨ py ⟩ - x ∎ - where - open Σ x renaming (fst to f~ ; snd to inv) - module inv = AreInverses inv - y : isEquiv _ _ f - y = {!!} - open Σ (toIso y) renaming (fst to f~' ; snd to inv') - py : toIso y ≡ (f~ , inv) - py = {!!} module _ {ℓa ℓb : Level} {A : Set ℓa} {B : Set ℓb} where open Cubical.PathPrelude using (_≃_) From ac01b786a7493af61246b321b1b97599f0132e4c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 22 Mar 2018 14:27:16 +0100 Subject: [PATCH 37/38] Cleanup --- src/Cat/Categories/Sets.agda | 11 +++++--- src/Cat/Category.agda | 55 +++++++++++++++++------------------- src/Cat/Prelude.agda | 4 +++ 3 files changed, 37 insertions(+), 33 deletions(-) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index c18c39a..05c64b3 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -219,6 +219,7 @@ module _ (ℓ : Level) where -- lem3 and the equivalence from lem4 step0 : Σ (A → B) isIso ≃ Σ (A → B) (isEquiv A B) step0 = lem3 {ℓc = lzero} (λ f → sym≃ (lem4 sA sB f)) + -- univalence step1 : Σ (A → B) (isEquiv A B) ≃ (A ≡ B) step1 = hh ⊙ h @@ -246,7 +247,7 @@ module _ (ℓ : Level) where step2 = sym≃ (lem2 (λ A → isSetIsProp) hA hB) -- Go from an isomorphism on sets to an isomorphism on homotopic sets - trivial? : (hA ≅ hB) ≃ Σ (A → B) isIso + trivial? : (hA ≅ hB) ≃ (A Eqv.≅ B) trivial? = sym≃ (fromIsomorphism res) where fwd : Σ (A → B) isIso → hA ≅ hB @@ -257,16 +258,18 @@ module _ (ℓ : Level) where bwd (f , g , x , y) = f , g , record { verso-recto = x ; recto-verso = y } res : Σ (A → B) isIso Eqv.≅ (hA ≅ hB) res = fwd , bwd , record { verso-recto = refl ; recto-verso = refl } + conclusion : (hA ≅ hB) ≃ (hA ≡ hB) conclusion = trivial? ⊙ step0 ⊙ step1 ⊙ step2 - thierry : (hA ≡ hB) ≃ (hA ≅ hB) - thierry = sym≃ conclusion + + univ≃ : (hA ≅ hB) ≃ (hA ≡ hB) + univ≃ = trivial? ⊙ step0 ⊙ step1 ⊙ step2 module _ (hA : Object) where open Σ hA renaming (proj₁ to A) eq1 : (Σ[ hB ∈ Object ] hA ≅ hB) ≡ (Σ[ hB ∈ Object ] hA ≡ hB) - eq1 = ua (lem3 (\ hB → sym≃ thierry)) + eq1 = ua (lem3 (\ hB → univ≃)) univalent[Contr] : isContr (Σ[ hB ∈ Object ] hA ≅ hB) univalent[Contr] = subst {P = isContr} (sym eq1) tres diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index cd8a9ec..70eb654 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -36,9 +36,9 @@ open import Cat.Prelude import Function ------------------ +------------------ -- * Categories -- ------------------ +------------------ -- | Raw categories -- @@ -111,16 +111,22 @@ record RawCategory (ℓa ℓb : Level) : Set (lsuc (ℓa ⊔ ℓb)) where -- | Univalence is indexed by a raw category as well as an identity proof. module Univalence (isIdentity : IsIdentity 𝟙) where + -- | The identity isomorphism idIso : (A : Object) → A ≅ A idIso A = 𝟙 , (𝟙 , isIdentity) - -- Lemma 9.1.4 in [HoTT] + -- | Extract an isomorphism from an equality + -- + -- [HoTT §9.1.4] id-to-iso : (A B : Object) → A ≡ B → A ≅ B id-to-iso A B eq = transp (\ i → A ≅ eq i) (idIso A) Univalent : Set (ℓa ⊔ ℓb) Univalent = {A B : Object} → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B) + -- A perhaps more readable version of univalence: + Univalent≃ = {A B : Object} → (A ≡ B) ≃ (A ≅ B) + -- | Equivalent formulation of univalence. Univalent[Contr] : Set _ Univalent[Contr] = ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) @@ -156,10 +162,14 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc rightIdentity : {A B : Object} {f : Arrow A B} → f ∘ 𝟙 ≡ f rightIdentity {A} {B} {f} = snd (isIdentity {A = A} {B} {f}) - -- Some common lemmas about categories. + ------------ + -- Lemmas -- + ------------ + + -- | Relation between iso- epi- and mono- morphisms. module _ {A B : Object} {X : Object} (f : Arrow A B) where - iso-is-epi : Isomorphism f → Epimorphism {X = X} f - iso-is-epi (f- , left-inv , right-inv) g₀ g₁ eq = begin + iso→epi : Isomorphism f → Epimorphism {X = X} f + iso→epi (f- , left-inv , right-inv) g₀ g₁ eq = begin g₀ ≡⟨ sym rightIdentity ⟩ g₀ ∘ 𝟙 ≡⟨ cong (_∘_ g₀) (sym right-inv) ⟩ g₀ ∘ (f ∘ f-) ≡⟨ isAssociative ⟩ @@ -169,8 +179,8 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc g₁ ∘ 𝟙 ≡⟨ rightIdentity ⟩ g₁ ∎ - iso-is-mono : Isomorphism f → Monomorphism {X = X} f - iso-is-mono (f- , left-inv , right-inv) g₀ g₁ eq = + iso→mono : Isomorphism f → Monomorphism {X = X} f + iso→mono (f- , left-inv , right-inv) g₀ g₁ eq = begin g₀ ≡⟨ sym leftIdentity ⟩ 𝟙 ∘ g₀ ≡⟨ cong (λ φ → φ ∘ g₀) (sym left-inv) ⟩ @@ -181,8 +191,13 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc 𝟙 ∘ g₁ ≡⟨ leftIdentity ⟩ g₁ ∎ - iso-is-epi-mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f - iso-is-epi-mono iso = iso-is-epi iso , iso-is-mono iso + iso→epi×mono : Isomorphism f → Epimorphism {X = X} f × Monomorphism {X = X} f + iso→epi×mono iso = iso→epi iso , iso→mono iso + + -- | The formulation of univalence expressed with _≃_ is trivially admissable - + -- just "forget" the equivalence. + univalent≃ : Univalent≃ + univalent≃ = _ , univalent -- | All projections are propositions. module Propositionality where @@ -206,24 +221,6 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc hh = arrowsAreSets _ _ (snd x) (snd y) in h i , hh i - module _ {A B : Object} {p q : A ≅ B} where - open Σ p renaming (proj₁ to pf) - open Σ (snd p) renaming (proj₁ to pg ; proj₂ to pAreInv) - open Σ q renaming (proj₁ to qf) - open Σ (snd q) renaming (proj₁ to qg ; proj₂ to qAreInv) - module _ (a : pf ≡ qf) (b : pg ≡ qg) where - private - open import Cubical.Sigma - open import Cubical.NType.Properties - -- Problem: How do I apply lempPropF twice? - cc : (λ i → IsInverseOf (a i) pg) [ pAreInv ≡ _ ] - cc = lemPropF (λ x → propIsInverseOf {A} {B} {x}) a - c : (λ i → IsInverseOf (a i) (b i)) [ pAreInv ≡ qAreInv ] - c = lemPropF (λ x → propIsInverseOf {A} {B} {{!!}}) {!cc!} - - ≅-equality : p ≡ q - ≅-equality i = a i , b i , c i - module _ {A B : Object} {f : Arrow A B} where isoIsProp : isProp (Isomorphism f) isoIsProp a@(g , η , ε) a'@(g' , η' , ε') = @@ -239,7 +236,7 @@ record IsCategory {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) : Set (lsuc g' ∎ propUnivalent : isProp Univalent - propUnivalent a b i = propPi (λ iso → propHasLevel ⟨-2⟩) a b i + propUnivalent a b i = propPi (λ iso → propIsContr) a b i -- | Propositionality of being a category module _ {ℓa ℓb : Level} (ℂ : RawCategory ℓa ℓb) where diff --git a/src/Cat/Prelude.agda b/src/Cat/Prelude.agda index c17fda0..f561330 100644 --- a/src/Cat/Prelude.agda +++ b/src/Cat/Prelude.agda @@ -24,6 +24,10 @@ open import Cubical.NType.Properties ( lemPropF ; lemSig ; lemSigP ; isSetIsProp ; propPi ; propHasLevel ; setPi ; propSet) public + +propIsContr : {ℓ : Level} → {A : Set ℓ} → isProp (isContr A) +propIsContr = propHasLevel ⟨-2⟩ + open import Cubical.Sigma using (setSig ; sigPresSet) public module _ (ℓ : Level) where From 4ae898dfe017403b6389f2057a0c6616190e0169 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 22 Mar 2018 14:51:43 +0100 Subject: [PATCH 38/38] Update backlog and changelog --- BACKLOG.md | 32 +++++++++++++++++++++++++------- CHANGELOG.md | 19 +++++++++++++++++++ 2 files changed, 44 insertions(+), 7 deletions(-) diff --git a/BACKLOG.md b/BACKLOG.md index c8fb54b..91d6b63 100644 --- a/BACKLOG.md +++ b/BACKLOG.md @@ -4,17 +4,37 @@ Backlog Prove postulates in `Cat.Wishlist`: * `ntypeCommulative : n ≤ m → HasLevel ⟨ n ⟩₋₂ A → HasLevel ⟨ m ⟩₋₂ A` +Prove that these two formulations of univalence are equivalent: + + ∀ A B → isEquiv (A ≡ B) (A ≅ B) (id-to-iso A B) + ∀ A → isContr (Σ[ X ∈ Object ] A ≅ X) + Prove univalence for the category of * the opposite category - * sets - This does not follow trivially from `Cubical.Univalence.univalence` because - objects are not `Set` but `hSet` * functors and natural transformations Prove: * `isProp (Product ...)` * `isProp (HasProducts ...)` +Ideas for future work +--------------------- + +It would be nice if my formulation of monads is not so "stand-alone" as it is at +the moment. + +We can built up the notion of monads and related concept in multiple ways as +demonstrated in the two equivalent formulations of monads (kleisli/monoidal): +There seems to be a category-theoretic approach and an approach more in the +style of functional programming as e.g. the related typeclasses in the +standard library of Haskell. + +It would be nice to build up this hierarchy in two ways: The +"category-theoretic" way and the "functional programming" way. + +Here is an overview of some of the concepts that need to be developed to acheive +this: + * Functor ✓ * Applicative Functor ✗ * Lax monoidal functor ✗ @@ -26,9 +46,7 @@ Prove: * Monoidal monad ✓ * Kleisli monad ✓ * Kleisli ≃ Monoidal ✓ - * Problem 2.3 in [voe] + * Problem 2.3 in [voe] ✓ * 1st contruction ~ monoidal ✓ * 2nd contruction ~ klesli ✓ - * 1st ≃ 2nd ✗ - I've managed to set this up so I should be able to reuse the proof that - Kleisli ≃ Monoidal, but I don't know why it doesn't typecheck. + * 1st ≃ 2nd ✓ diff --git a/CHANGELOG.md b/CHANGELOG.md index 625d640..42ab3e0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,6 +1,25 @@ Changelog ========= +Version 1.4.1 +------------- +Defines a module to work with equivalence providing a way to go between +equivalences and quasi-inverses (in the parlance of HoTT). + +Finishes the proof that the category of homotopy-sets are univalent. + +Defines a custom "prelude" module that wraps the `cubical` library and provides +a few utilities. + +Reorders Category.isIdentity such that the left projection is left identity. + +Include some text for the half-time report. + +Renames IsProduct.isProduct to IsProduct.ump to avoid ambiguity in some +circumstances. + +[WIP]: Adds some stuff about propositionality for products. + Version 1.4.0 ------------- Adds documentation to a number of modules.