From cd98736d028b27d168f7b0bad05d1ebc0f5ad9b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 25 Feb 2018 15:21:38 +0100 Subject: [PATCH] Add documentation in Category-module --- src/Cat/Category.agda | 146 +++++++++++++++++++++++++++++------------- 1 file changed, 103 insertions(+), 43 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index df13850..7ba7eb9 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -1,3 +1,32 @@ +-- | 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 @@ -16,6 +45,11 @@ 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) βˆƒ! = βˆƒ!β‰ˆ _≑_ @@ -25,6 +59,15 @@ open import Cat.Wishlist 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 @@ -35,12 +78,16 @@ record RawCategory (β„“a β„“b : Level) : Set (lsuc (β„“a βŠ” β„“b)) where 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) @@ -93,12 +140,16 @@ module Univalence {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) where id-to-iso : (A B : Object) β†’ A ≑ B β†’ A β‰… B id-to-iso A B eq = transp (\ i β†’ A β‰… eq i) (idIso A) - -- TODO: might want to implement isEquiv - -- differently, there are 3 - -- equivalent formulations in the book. 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 @@ -107,6 +158,8 @@ record IsCategory {β„“a β„“b : Level} (β„‚ : RawCategory β„“a β„“b) : Set (lsuc 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 @@ -134,7 +187,10 @@ 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 --- `IsCategory` is a mere proposition. +-- | 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 @@ -217,6 +273,9 @@ module _ {β„“a β„“b : Level} {C : RawCategory β„“a β„“b} where 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 @@ -224,6 +283,7 @@ record Category (β„“a β„“b : Level) : Set (lsuc (β„“a βŠ” β„“b)) where 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 @@ -232,48 +292,48 @@ module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where _[_∘_] : {A B C : Object} β†’ (g : Arrow B C) β†’ (f : Arrow A B) β†’ Arrow A C _[_∘_] = _∘_ -module _ {β„“a β„“b : Level} (β„‚ : Category β„“a β„“b) where - private +-- | 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 _∘_ - 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 = {!!} - 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 - 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 _) = _∘_ --- 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 more than 20!! -module _ {β„“a β„“b : Level} {β„‚ : Category β„“a β„“b} where - private - open RawCategory - module C = Category β„‚ - rawOp : Category.raw (Opposite (Opposite β„‚)) ≑ Category.raw β„‚ - Object (rawOp _) = C.Object - Arrow (rawOp _) = C.Arrow - πŸ™ (rawOp _) = C.πŸ™ - _∘_ (rawOp _) = C._∘_ - open Category - open IsCategory - module IsCat = IsCategory (β„‚ .isCategory) - rawIsCat : (i : I) β†’ IsCategory (rawOp i) - isAssociative (rawIsCat i) = IsCat.isAssociative - isIdentity (rawIsCat i) = IsCat.isIdentity - arrowsAreSets (rawIsCat i) = IsCat.arrowsAreSets - univalent (rawIsCat i) = IsCat.univalent + -- TODO: Define and use Monad≑ + oppositeIsInvolution : opposite (opposite β„‚) ≑ β„‚ + Category.raw (oppositeIsInvolution i) = rawInv i + Category.isCategory (oppositeIsInvolution x) = {!!} - Opposite-is-involution : Opposite (Opposite β„‚) ≑ β„‚ - raw (Opposite-is-involution i) = rawOp i - isCategory (Opposite-is-involution i) = rawIsCat i +open Opposite public renaming (opposite to Opposite)