-- | Univalent categories -- -- This module defines: -- -- Categories -- ========== -- -- Types -- ------ -- -- Object, Arrow -- -- Data -- ---- -- πŸ™; the identity arrow -- _∘_; function composition -- -- Laws -- ---- -- -- associativity, identity, arrows form sets, univalence. -- -- Lemmas -- ------ -- -- Propositionality for all laws about the category. -- -- TODO: An equality principle for categories that focuses on the pure data-part. -- {-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Category where open import Agda.Primitive open import Data.Unit.Base open import Data.Product renaming ( proj₁ to fst ; projβ‚‚ to snd ; βˆƒ! to βˆƒ!β‰ˆ ) open import Data.Empty import Function open import Cubical open import Cubical.NType.Properties using ( propIsEquiv ) 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 -- ----------------- -- | Raw categories -- -- This record desribes the data that a category consist of as well as some laws -- about these. The laws defined are the types the propositions - not the -- witnesses to them! record RawCategory (β„“a β„“b : Level) : Set (lsuc (β„“a βŠ” β„“b)) where no-eta-equality field Object : Set β„“a Arrow : Object β†’ Object β†’ Set β„“b πŸ™ : {A : Object} β†’ Arrow A A _∘_ : {A B C : Object} β†’ Arrow B C β†’ Arrow A B β†’ Arrow A C infixl 10 _∘_ -- | Operations on data domain : { a b : Object } β†’ Arrow a b β†’ Object domain {a = a} _ = a codomain : { a b : Object } β†’ Arrow a b β†’ Object codomain {b = b} _ = b -- | Laws about the data -- TODO: It seems counter-intuitive that the normal-form is on the -- right-hand-side. IsAssociative : Set (β„“a βŠ” β„“b) IsAssociative = βˆ€ {A B C D} {f : Arrow A B} {g : Arrow B C} {h : Arrow C D} β†’ h ∘ (g ∘ f) ≑ (h ∘ g) ∘ f IsIdentity : ({A : Object} β†’ Arrow A A) β†’ Set (β„“a βŠ” β„“b) IsIdentity id = {A B : Object} {f : Arrow A B} β†’ f ∘ id ≑ f Γ— id ∘ f ≑ f ArrowsAreSets : Set (β„“a βŠ” β„“b) ArrowsAreSets = βˆ€ {A B : Object} β†’ isSet (Arrow A B) IsInverseOf : βˆ€ {A B} β†’ (Arrow A B) β†’ (Arrow B A) β†’ Set β„“b IsInverseOf = Ξ» f g β†’ g ∘ f ≑ πŸ™ Γ— f ∘ g ≑ πŸ™ Isomorphism : βˆ€ {A B} β†’ (f : Arrow A B) β†’ Set β„“b Isomorphism {A} {B} f = Ξ£[ g ∈ Arrow B A ] IsInverseOf f g _β‰…_ : (A B : Object) β†’ Set β„“b _β‰…_ A B = Ξ£[ f ∈ Arrow A B ] (Isomorphism f) module _ {A B : Object} where Epimorphism : {X : Object } β†’ (f : Arrow A B) β†’ Set β„“b Epimorphism {X} f = ( gβ‚€ g₁ : Arrow B X ) β†’ gβ‚€ ∘ f ≑ g₁ ∘ f β†’ gβ‚€ ≑ g₁ Monomorphism : {X : Object} β†’ (f : Arrow A B) β†’ Set β„“b Monomorphism {X} f = ( gβ‚€ g₁ : Arrow X A ) β†’ f ∘ gβ‚€ ≑ f ∘ g₁ β†’ gβ‚€ ≑ g₁ IsInitial : Object β†’ Set (β„“a βŠ” β„“b) IsInitial I = {X : Object} β†’ isContr (Arrow I X) IsTerminal : Object β†’ Set (β„“a βŠ” β„“b) IsTerminal T = {X : Object} β†’ isContr (Arrow X T) Initial : Set (β„“a βŠ” β„“b) Initial = Ξ£ Object IsInitial Terminal : Set (β„“a βŠ” β„“b) Terminal = Ξ£ Object IsTerminal -- Univalence is indexed by a raw category as well as an identity proof. module Univalence {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) where open RawCategory β„‚ module _ (isIdentity : IsIdentity πŸ™) where idIso : (A : Object) β†’ A β‰… A idIso A = πŸ™ , (πŸ™ , isIdentity) -- Lemma 9.1.4 in [HoTT] 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) -- | The mere proposition of being a category. -- -- Also defines a few lemmas: -- -- iso-is-epi : Isomorphism f β†’ Epimorphism {X = X} f -- iso-is-mono : Isomorphism f β†’ Monomorphism {X = X} f -- 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 -- 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β‚€ ∘ πŸ™ β‰‘βŸ¨ 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₁ ∎ 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β‚€ β‰‘βŸ¨ 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₁ ∎ 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 _ {β„“a β„“b : Level} {C : RawCategory β„“a β„“b} where open RawCategory C module _ (β„‚ : IsCategory C) where open IsCategory β„‚ using (isAssociative ; arrowsAreSets ; isIdentity ; Univalent) open import Cubical.NType open import Cubical.NType.Properties propIsAssociative : isProp IsAssociative propIsAssociative x y i = arrowsAreSets _ _ x y i propIsIdentity : βˆ€ {f : βˆ€ {A} β†’ Arrow A A} β†’ isProp (IsIdentity f) propIsIdentity a b i = arrowsAreSets _ _ (fst a) (fst b) i , arrowsAreSets _ _ (snd a) (snd b) i propArrowIsSet : isProp (βˆ€ {A B} β†’ isSet (Arrow A B)) propArrowIsSet a b i = isSetIsProp a b i propIsInverseOf : βˆ€ {A B f g} β†’ isProp (IsInverseOf {A} {B} f g) propIsInverseOf x y = Ξ» i β†’ let h : fst x ≑ fst y h = arrowsAreSets _ _ (fst x) (fst y) hh : snd x ≑ snd y hh = arrowsAreSets _ _ (snd x) (snd y) in h i , hh i module _ {A B : Object} {f : Arrow A B} where isoIsProp : isProp (Isomorphism f) isoIsProp a@(g , Ξ· , Ξ΅) a'@(g' , Ξ·' , Ξ΅') = lemSig (Ξ» g β†’ propIsInverseOf) a a' geq where open Cubical.NType.Properties geq : g ≑ g' geq = begin g β‰‘βŸ¨ sym (fst isIdentity) ⟩ g ∘ πŸ™ β‰‘βŸ¨ cong (Ξ» Ο† β†’ g ∘ Ο†) (sym Ξ΅') ⟩ g ∘ (f ∘ g') β‰‘βŸ¨ isAssociative ⟩ (g ∘ f) ∘ g' β‰‘βŸ¨ cong (Ξ» Ο† β†’ Ο† ∘ g') Ξ· ⟩ πŸ™ ∘ g' β‰‘βŸ¨ snd isIdentity ⟩ g' ∎ propUnivalent : isProp (Univalent isIdentity) propUnivalent a b i = propPi (Ξ» iso β†’ propHasLevel ⟨-2⟩) a b i private module _ (x y : IsCategory C) where module IC = IsCategory module X = IsCategory x module Y = IsCategory y open Univalence C -- 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 -- adverse effects this may have. isIdentity : (Ξ» _ β†’ IsIdentity πŸ™) [ X.isIdentity ≑ Y.isIdentity ] isIdentity = propIsIdentity x X.isIdentity Y.isIdentity done : x ≑ y U : βˆ€ {a : IsIdentity πŸ™} β†’ (Ξ» _ β†’ IsIdentity πŸ™) [ X.isIdentity ≑ a ] β†’ (b : Univalent a) β†’ Set _ U eqwal bbb = (Ξ» i β†’ Univalent (eqwal i)) [ X.univalent ≑ bbb ] P : (y : IsIdentity πŸ™) β†’ (Ξ» _ β†’ IsIdentity πŸ™) [ X.isIdentity ≑ y ] β†’ Set _ P y eq = βˆ€ (b' : Univalent y) β†’ U eq b' helper : βˆ€ (b' : Univalent X.isIdentity) β†’ (Ξ» _ β†’ Univalent X.isIdentity) [ X.univalent ≑ b' ] helper univ = propUnivalent x X.univalent univ foo = pathJ P helper Y.isIdentity isIdentity eqUni : U isIdentity Y.univalent eqUni = foo Y.univalent IC.isAssociative (done i) = propIsAssociative x X.isAssociative Y.isAssociative i IC.isIdentity (done i) = isIdentity i IC.arrowsAreSets (done i) = propArrowIsSet x X.arrowsAreSets Y.arrowsAreSets i IC.univalent (done i) = eqUni i propIsCategory : isProp (IsCategory C) propIsCategory = done -- | Univalent categories -- -- Just bundles up the data with witnesses inhabting the propositions. record Category (β„“a β„“b : Level) : Set (lsuc (β„“a βŠ” β„“b)) where field raw : RawCategory β„“a β„“b {{isCategory}} : IsCategory raw open IsCategory isCategory public -- | Syntax for arrows- and composition in a given category. module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where open Category β„‚ _[_,_] : (A : Object) β†’ (B : Object) β†’ Set β„“b _[_,_] = Arrow _[_∘_] : {A B C : Object} β†’ (g : Arrow B C) β†’ (f : Arrow A B) β†’ Arrow A C _[_∘_] = _∘_ -- | The opposite category -- -- The opposite category is the category where the direction of the arrows are -- flipped. module Opposite {β„“a β„“b : Level} where module _ (β„‚ : Category β„“a β„“b) where open Category β„‚ private opRaw : RawCategory β„“a β„“b RawCategory.Object opRaw = Object RawCategory.Arrow opRaw = Function.flip Arrow RawCategory.πŸ™ opRaw = πŸ™ RawCategory._∘_ opRaw = Function.flip _∘_ opIsCategory : IsCategory opRaw IsCategory.isAssociative opIsCategory = sym isAssociative IsCategory.isIdentity opIsCategory = swap isIdentity IsCategory.arrowsAreSets opIsCategory = arrowsAreSets IsCategory.univalent opIsCategory = {!!} opposite : Category β„“a β„“b raw opposite = opRaw Category.isCategory opposite = opIsCategory -- As demonstrated here a side-effect of having no-eta-equality on constructors -- means that we need to pick things apart to show that things are indeed -- definitionally equal. I.e; a thing that would normally be provable in one -- line now takes 13!! Admittedly it's a simple proof. module _ {β„‚ : Category β„“a β„“b} where open Category β„‚ private -- Since they really are definitionally equal we just need to pick apart -- the data-type. rawInv : Category.raw (opposite (opposite β„‚)) ≑ raw RawCategory.Object (rawInv _) = Object RawCategory.Arrow (rawInv _) = Arrow RawCategory.πŸ™ (rawInv _) = πŸ™ RawCategory._∘_ (rawInv _) = _∘_ -- TODO: Define and use Monad≑ oppositeIsInvolution : opposite (opposite β„‚) ≑ β„‚ Category.raw (oppositeIsInvolution i) = rawInv i Category.isCategory (oppositeIsInvolution x) = {!!} open Opposite public