-- | 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. {-# 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 ; lemPropF ) 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 _>>>_ : {A B C : Object} β†’ (Arrow A B) β†’ (Arrow B C) β†’ Arrow A C f >>> g = g ∘ f -- | Laws about the data -- FIXME 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. -- -- 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 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) -- 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. -- -- Also defines a few lemmas: -- -- iso-is-epi : Isomorphism f β†’ Epimorphism {X = X} f -- iso-is-mono : Isomorphism f β†’ Monomorphism {X = X} f -- -- Sans `univalent` this would be what is referred to as a pre-category in -- [HoTT]. record IsCategory {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) : Set (lsuc (β„“a βŠ” β„“b)) where open RawCategory β„‚ public open Univalence β„‚ public 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 Propositionality {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) where open RawCategory β„‚ module _ (β„‚ : IsCategory β„‚) 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 β„‚) 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 -- 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 U : βˆ€ {a : IsIdentity πŸ™} β†’ (Ξ» _ β†’ IsIdentity πŸ™) [ X.isIdentity ≑ a ] β†’ (b : Univalent a) β†’ Set _ U eqwal univ = (Ξ» i β†’ Univalent (eqwal i)) [ X.univalent ≑ univ ] P : (y : IsIdentity πŸ™) β†’ (Ξ» _ β†’ IsIdentity πŸ™) [ X.isIdentity ≑ y ] β†’ Set _ 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 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 propIsCategory : isProp (IsCategory β„‚) propIsCategory = done -- | Univalent categories -- -- Just bundles up the data with witnesses inhabiting the propositions. record Category (β„“a β„“b : Level) : Set (lsuc (β„“a βŠ” β„“b)) where field raw : RawCategory β„“a β„“b {{isCategory}} : IsCategory raw open IsCategory isCategory public -- The fact that being a category is a mere proposition gives rise to this -- equality principle for categories. module _ {β„“a β„“b : Level} {β„‚ 𝔻 : Category β„“a β„“b} where private module β„‚ = Category β„‚ module 𝔻 = Category 𝔻 module _ (rawEq : β„‚.raw ≑ 𝔻.raw) where private isCategoryEq : (Ξ» i β†’ IsCategory (rawEq i)) [ β„‚.isCategory ≑ 𝔻.isCategory ] isCategoryEq = lemPropF Propositionality.propIsCategory rawEq Category≑ : β„‚ ≑ 𝔻 Category≑ i = record { raw = rawEq i ; isCategory = isCategoryEq i } -- | Syntax for arrows- and composition in a given category. module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where 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 private module β„‚ = Category β„‚ opRaw : RawCategory β„“a β„“b RawCategory.Object opRaw = β„‚.Object RawCategory.Arrow opRaw = Function.flip β„‚.Arrow RawCategory.πŸ™ opRaw = β„‚.πŸ™ RawCategory._∘_ opRaw = Function.flip β„‚._∘_ open RawCategory opRaw open Univalence opRaw isIdentity : IsIdentity πŸ™ isIdentity = swap β„‚.isIdentity module _ {A B : β„‚.Object} where univalent : isEquiv (A ≑ B) (A β‰… B) (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 flipFiber (eq , eqIso) = sym eq , {!!} snd (univalent iso) = {!!} isCategory : IsCategory opRaw IsCategory.isAssociative isCategory = sym β„‚.isAssociative IsCategory.isIdentity isCategory = isIdentity IsCategory.arrowsAreSets isCategory = β„‚.arrowsAreSets IsCategory.univalent isCategory = univalent opposite : Category β„“a β„“b Category.raw opposite = opRaw Category.isCategory opposite = isCategory -- 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 _) = _∘_ oppositeIsInvolution : opposite (opposite β„‚) ≑ β„‚ oppositeIsInvolution = Category≑ rawInv open Opposite public