diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 916ca9a..c57e183 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -70,16 +70,49 @@ module _ {β„“ β„“' : Level} where ; πŸ™ = identity ; _βŠ•_ = functor-comp -- What gives here? Why can I not name the variables directly? - ; assoc = Ξ» {_ _ _ _ f g h} β†’ assc {f = f} {g = g} {h = h} - ; ident = ident-r , ident-l + ; isCategory = {!!} +-- ; assoc = Ξ» {_ _ _ _ f g h} β†’ assc {f = f} {g = g} {h = h} +-- ; ident = ident-r , ident-l } -module _ {β„“ : Level} (C D : Category β„“ β„“) where +module _ {β„“ : Level} (C D : Category β„“ β„“) where private - proj₁ : Arrow CatCat (catProduct C D) C + :Object: = C .Object Γ— D .Object + :Arrow: : :Object: β†’ :Object: β†’ Set β„“ + :Arrow: (c , d) (c' , d') = Arrow C c c' Γ— Arrow D d d' + :πŸ™: : {o : :Object:} β†’ :Arrow: o o + :πŸ™: = C .πŸ™ , D .πŸ™ + _:βŠ•:_ : + {a b c : :Object:} β†’ + :Arrow: b c β†’ + :Arrow: a b β†’ + :Arrow: a c + _:βŠ•:_ = Ξ» { (bc∈C , bc∈D) (ab∈C , ab∈D) β†’ (C ._βŠ•_) bc∈C ab∈C , D ._βŠ•_ bc∈D ab∈D} + + instance + :isCategory: : IsCategory :Object: :Arrow: :πŸ™: _:βŠ•:_ + :isCategory: = record + { assoc = eqpair C.assoc D.assoc + ; ident + = eqpair (fst C.ident) (fst D.ident) + , eqpair (snd C.ident) (snd D.ident) + } + where + open module C = IsCategory (C .isCategory) + open module D = IsCategory (D .isCategory) + + :product: : Category β„“ β„“ + :product: = record + { Object = :Object: + ; Arrow = :Arrow: + ; πŸ™ = :πŸ™: + ; _βŠ•_ = _:βŠ•:_ + } + + proj₁ : Arrow CatCat :product: C proj₁ = record { func* = fst ; funcβ†’ = fst ; ident = refl ; distrib = refl } - projβ‚‚ : Arrow CatCat (catProduct C D) D + projβ‚‚ : Arrow CatCat :product: D projβ‚‚ = record { func* = snd ; funcβ†’ = snd ; ident = refl ; distrib = refl } module _ {X : Object (CatCat {β„“} {β„“})} (x₁ : Arrow CatCat X C) (xβ‚‚ : Arrow CatCat X D) where @@ -88,7 +121,7 @@ module _ {β„“ : Level} (C D : Category β„“ β„“) where -- ident' : {c : Object X} β†’ ((funcβ†’ x₁) {dom = c} (πŸ™ X) , (funcβ†’ xβ‚‚) {dom = c} (πŸ™ X)) ≑ πŸ™ (catProduct C D) -- ident' {c = c} = lift-eq (ident x₁) (ident xβ‚‚) - x : Functor X (catProduct C D) + x : Functor X :product: x = record { func* = Ξ» x β†’ (func* x₁) x , (func* xβ‚‚) x ; funcβ†’ = Ξ» x β†’ funcβ†’ x₁ x , funcβ†’ xβ‚‚ x @@ -116,7 +149,7 @@ module _ {β„“ : Level} (C D : Category β„“ β„“) where product : Product {β„‚ = CatCat} C D product = record - { obj = catProduct C D + { obj = :product: ; proj₁ = proj₁ ; projβ‚‚ = projβ‚‚ } diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 0f2fce9..b398aa9 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -160,6 +160,5 @@ Rel = record ; Arrow = Ξ» S R β†’ Subset (S Γ— R) ; πŸ™ = Ξ» {S} β†’ Diag S ; _βŠ•_ = Ξ» {A B C} S R β†’ Ξ» {( a , c ) β†’ Ξ£[ b ∈ B ] ( (a , b) ∈ R Γ— (b , c) ∈ S )} - ; assoc = funExt is-assoc - ; ident = funExt ident-l , funExt ident-r + ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r } } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 5993b4b..3579b52 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -9,21 +9,18 @@ open import Data.Product renaming (proj₁ to fst ; projβ‚‚ to snd) open import Cat.Category open import Cat.Functor - --- Sets are built-in to Agda. The set of all small sets is called Set. - -Fun : {β„“ : Level} β†’ ( T U : Set β„“ ) β†’ Set β„“ -Fun T U = T β†’ U +open Category Sets : {β„“ : Level} β†’ Category (lsuc β„“) β„“ Sets {β„“} = record { Object = Set β„“ - ; Arrow = Ξ» T U β†’ Fun {β„“} T U - ; πŸ™ = Ξ» x β†’ x - ; _βŠ•_ = Ξ» g f x β†’ g ( f x ) - ; assoc = refl - ; ident = funExt (Ξ» x β†’ refl) , funExt (Ξ» x β†’ refl) + ; Arrow = Ξ» T U β†’ T β†’ U + ; πŸ™ = id + ; _βŠ•_ = _βˆ˜β€²_ + ; isCategory = record { assoc = refl ; ident = funExt (Ξ» _ β†’ refl) , funExt (Ξ» _ β†’ refl) } } + where + open import Function -- Covariant Presheaf Representable : {β„“ β„“' : Level} β†’ (β„‚ : Category β„“ β„“') β†’ Set (β„“ βŠ” lsuc β„“') @@ -32,13 +29,13 @@ Representable {β„“' = β„“'} β„‚ = Functor β„‚ (Sets {β„“'}) -- The "co-yoneda" embedding. representable : βˆ€ {β„“ β„“'} {β„‚ : Category β„“ β„“'} β†’ Category.Object β„‚ β†’ Representable β„‚ representable {β„‚ = β„‚} A = record - { func* = Ξ» B β†’ β„‚.Arrow A B - ; funcβ†’ = Ξ» f g β†’ f β„‚.βŠ• g - ; ident = funExt Ξ» _ β†’ snd β„‚.ident - ; distrib = funExt Ξ» x β†’ sym β„‚.assoc + { func* = Ξ» B β†’ β„‚ .Arrow A B + ; funcβ†’ = β„‚ ._βŠ•_ + ; ident = funExt Ξ» _ β†’ snd ident + ; distrib = funExt Ξ» x β†’ sym assoc } where - open module β„‚ = Category β„‚ + open IsCategory (β„‚ .isCategory) -- Contravariant Presheaf Presheaf : βˆ€ {β„“ β„“'} (β„‚ : Category β„“ β„“') β†’ Set (β„“ βŠ” lsuc β„“') @@ -47,10 +44,10 @@ Presheaf {β„“' = β„“'} β„‚ = Functor (Opposite β„‚) (Sets {β„“'}) -- Alternate name: `yoneda` presheaf : {β„“ β„“' : Level} {β„‚ : Category β„“ β„“'} β†’ Category.Object (Opposite β„‚) β†’ Presheaf β„‚ presheaf {β„‚ = β„‚} B = record - { func* = Ξ» A β†’ β„‚.Arrow A B - ; funcβ†’ = Ξ» f g β†’ g β„‚.βŠ• f - ; ident = funExt Ξ» x β†’ fst β„‚.ident - ; distrib = funExt Ξ» x β†’ β„‚.assoc + { func* = Ξ» A β†’ β„‚ .Arrow A B + ; funcβ†’ = Ξ» f g β†’ β„‚ ._βŠ•_ g f + ; ident = funExt Ξ» x β†’ fst ident + ; distrib = funExt Ξ» x β†’ assoc } where - open module β„‚ = Category β„‚ + open IsCategory (β„‚ .isCategory) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index c388f77..a881c71 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -24,6 +24,20 @@ syntax βˆƒ!-syntax (Ξ» x β†’ B) = βˆƒ![ x ] B postulate undefined : {β„“ : Level} β†’ {A : Set β„“} β†’ A +record IsCategory {β„“ β„“' : Level} + (Object : Set β„“) + (Arrow : Object β†’ Object β†’ Set β„“') + (πŸ™ : {o : Object} β†’ Arrow o o) + (_βŠ•_ : { a b c : Object } β†’ Arrow b c β†’ Arrow a b β†’ Arrow a c) + : Set (lsuc (β„“' βŠ” β„“)) where + field + assoc : {A B C D : Object} { f : Arrow A B } { g : Arrow B C } { h : Arrow C D } + β†’ h βŠ• (g βŠ• f) ≑ (h βŠ• g) βŠ• f + ident : {A B : Object} {f : Arrow A B} + β†’ f βŠ• πŸ™ ≑ f Γ— πŸ™ βŠ• f ≑ f + +-- open IsCategory public + record Category (β„“ β„“' : Level) : Set (lsuc (β„“' βŠ” β„“)) where -- adding no-eta-equality can speed up type-checking. no-eta-equality @@ -32,17 +46,14 @@ record Category (β„“ β„“' : Level) : Set (lsuc (β„“' βŠ” β„“)) where Arrow : Object β†’ Object β†’ Set β„“' πŸ™ : {o : Object} β†’ Arrow o o _βŠ•_ : { a b c : Object } β†’ Arrow b c β†’ Arrow a b β†’ Arrow a c - assoc : { A B C D : Object } { f : Arrow A B } { g : Arrow B C } { h : Arrow C D } - β†’ h βŠ• (g βŠ• f) ≑ (h βŠ• g) βŠ• f - ident : { A B : Object } { f : Arrow A B } - β†’ f βŠ• πŸ™ ≑ f Γ— πŸ™ βŠ• f ≑ f + {{isCategory}} : IsCategory Object Arrow πŸ™ _βŠ•_ infixl 45 _βŠ•_ domain : { a b : Object } β†’ Arrow a b β†’ Object domain {a = a} _ = a codomain : { a b : Object } β†’ Arrow a b β†’ Object codomain {b = b} _ = b -open Category public +open Category module _ {β„“ β„“' : Level} {β„‚ : Category β„“ β„“'} { A B : β„‚ .Object } where private @@ -61,26 +72,30 @@ module _ {β„“ β„“' : Level} {β„‚ : Category β„“ β„“'} { A B : β„‚ .Object } wher iso-is-epi : βˆ€ {X} (f : β„‚.Arrow A B) β†’ Isomorphism f β†’ Epimorphism {X = X} f iso-is-epi f (f- , left-inv , right-inv) gβ‚€ g₁ eq = begin - gβ‚€ β‰‘βŸ¨ sym (fst β„‚.ident) ⟩ + gβ‚€ β‰‘βŸ¨ sym (fst ident) ⟩ gβ‚€ + β„‚.πŸ™ β‰‘βŸ¨ cong (_+_ gβ‚€) (sym right-inv) ⟩ - gβ‚€ + (f + f-) β‰‘βŸ¨ β„‚.assoc ⟩ + gβ‚€ + (f + f-) β‰‘βŸ¨ assoc ⟩ (gβ‚€ + f) + f- β‰‘βŸ¨ cong (Ξ» x β†’ x + f-) eq ⟩ - (g₁ + f) + f- β‰‘βŸ¨ sym β„‚.assoc ⟩ + (g₁ + f) + f- β‰‘βŸ¨ sym assoc ⟩ g₁ + (f + f-) β‰‘βŸ¨ cong (_+_ g₁) right-inv ⟩ - g₁ + β„‚.πŸ™ β‰‘βŸ¨ fst β„‚.ident ⟩ + g₁ + β„‚.πŸ™ β‰‘βŸ¨ fst ident ⟩ g₁ ∎ + where + open IsCategory β„‚.isCategory iso-is-mono : βˆ€ {X} (f : β„‚.Arrow A B ) β†’ Isomorphism f β†’ Monomorphism {X = X} f iso-is-mono f (f- , (left-inv , right-inv)) gβ‚€ g₁ eq = begin - gβ‚€ β‰‘βŸ¨ sym (snd β„‚.ident) ⟩ + gβ‚€ β‰‘βŸ¨ sym (snd ident) ⟩ β„‚.πŸ™ + gβ‚€ β‰‘βŸ¨ cong (Ξ» x β†’ x + gβ‚€) (sym left-inv) ⟩ - (f- + f) + gβ‚€ β‰‘βŸ¨ sym β„‚.assoc ⟩ + (f- + f) + gβ‚€ β‰‘βŸ¨ sym assoc ⟩ f- + (f + gβ‚€) β‰‘βŸ¨ cong (_+_ f-) eq ⟩ - f- + (f + g₁) β‰‘βŸ¨ β„‚.assoc ⟩ + f- + (f + g₁) β‰‘βŸ¨ assoc ⟩ (f- + f) + g₁ β‰‘βŸ¨ cong (Ξ» x β†’ x + g₁) left-inv ⟩ - β„‚.πŸ™ + g₁ β‰‘βŸ¨ snd β„‚.ident ⟩ + β„‚.πŸ™ + g₁ β‰‘βŸ¨ snd ident ⟩ g₁ ∎ + where + open IsCategory β„‚.isCategory iso-is-epi-mono : βˆ€ {X} (f : β„‚.Arrow A B ) β†’ Isomorphism f β†’ Epimorphism {X = X} f Γ— Monomorphism {X = X} f iso-is-epi-mono f iso = iso-is-epi f iso , iso-is-mono f iso @@ -118,49 +133,27 @@ record Product {β„“ β„“' : Level} {β„‚ : Category β„“ β„“'} (A B : β„‚ .Object) projβ‚‚ : β„‚ .Arrow obj B {{isProduct}} : IsProduct β„‚ proj₁ projβ‚‚ -mutual - catProduct : βˆ€ {β„“} (C D : Category β„“ β„“) β†’ Category β„“ β„“ - catProduct C D = +-- Two pairs are equal if their components are equal. +eqpair : βˆ€ {β„“a β„“b} {A : Set β„“a} {B : Set β„“b} {a a' : A} {b b' : B} + β†’ a ≑ a' β†’ b ≑ b' β†’ (a , b) ≑ (a' , b') +eqpair eqa eqb i = eqa i , eqb i + +module _ {β„“ β„“' : Level} (β„‚ : Category β„“ β„“') where + private + instance + _ : IsCategory (β„‚ .Object) (flip (β„‚ .Arrow)) (β„‚ .πŸ™) (flip (β„‚ ._βŠ•_)) + _ = record { assoc = sym assoc ; ident = swap ident } + where + open IsCategory (β„‚ .isCategory) + + Opposite : Category β„“ β„“' + Opposite = record - { Object = C.Object Γ— D.Object - -- Why does "outlining with `arrowProduct` not work? - ; Arrow = Ξ» {(c , d) (c' , d') β†’ Arrow C c c' Γ— Arrow D d d'} - ; πŸ™ = C.πŸ™ , D.πŸ™ - ; _βŠ•_ = Ξ» { (bc∈C , bc∈D) (ab∈C , ab∈D) β†’ bc∈C C.βŠ• ab∈C , bc∈D D.βŠ• ab∈D} - ; assoc = eqpair C.assoc D.assoc - ; ident = - let (Cl , Cr) = C.ident - (Dl , Dr) = D.ident - in eqpair Cl Dl , eqpair Cr Dr + { Object = β„‚ .Object + ; Arrow = flip (β„‚ .Arrow) + ; πŸ™ = β„‚ .πŸ™ + ; _βŠ•_ = flip (β„‚ ._βŠ•_) } - where - open module C = Category C - open module D = Category D - -- Two pairs are equal if their components are equal. - eqpair : βˆ€ {β„“a β„“b} {A : Set β„“a} {B : Set β„“b} {a a' : A} {b b' : B} - β†’ a ≑ a' β†’ b ≑ b' β†’ (a , b) ≑ (a' , b') - eqpair eqa eqb i = eqa i , eqb i - - - -- arrowProduct : βˆ€ {β„“} {C D : Category {β„“} {β„“}} β†’ (Object C) Γ— (Object D) β†’ (Object C) Γ— (Object D) β†’ Set β„“ - -- arrowProduct = {!!} - - -- Arrows in the product-category - arrowProduct : βˆ€ {β„“} {C D : Category β„“ β„“} (c d : Object (catProduct C D)) β†’ Set β„“ - arrowProduct {C = C} {D = D} (c , d) (c' , d') = Arrow C c c' Γ— Arrow D d d' - -Opposite : βˆ€ {β„“ β„“'} β†’ Category β„“ β„“' β†’ Category β„“ β„“' -Opposite β„‚ = - record - { Object = β„‚.Object - ; Arrow = Ξ» A B β†’ β„‚.Arrow B A - ; πŸ™ = β„‚.πŸ™ - ; _βŠ•_ = Ξ» g f β†’ f β„‚.βŠ• g - ; assoc = sym β„‚.assoc - ; ident = swap β„‚.ident - } - where - open module β„‚ = Category β„‚ -- A consequence of no-eta-equality; `Opposite-is-involution` is no longer -- definitional - i.e.; you must match on the fields: diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda index d6ca6ac..98305a6 100644 --- a/src/Cat/Category/Free.agda +++ b/src/Cat/Category/Free.agda @@ -34,6 +34,5 @@ module _ {β„“ β„“' : Level} (β„‚ : Category β„“ β„“') where ; Arrow = Path ; πŸ™ = Ξ» {o} β†’ emptyPath o ; _βŠ•_ = Ξ» {a b c} β†’ concatenate {a} {b} {c} - ; assoc = p-assoc - ; ident = ident-r , ident-l + ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l } } diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index adfec58..f415fc1 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -7,14 +7,13 @@ open import Cat.Functor open import Cat.Categories.Sets module _ {β„“a β„“a' β„“b β„“b'} where - Exponential : Category β„“a β„“a' β†’ Category β„“b β„“b' β†’ Category ? ? + Exponential : Category β„“a β„“a' β†’ Category β„“b β„“b' β†’ Category {!!} {!!} Exponential A B = record { Object = {!!} ; Arrow = {!!} ; πŸ™ = {!!} ; _βŠ•_ = {!!} - ; assoc = {!!} - ; ident = {!!} + ; isCategory = ? } _⇑_ = Exponential diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda index 025e202..b10afba 100644 --- a/src/Cat/Cubical.agda +++ b/src/Cat/Cubical.agda @@ -49,6 +49,5 @@ module _ {β„“ β„“' : Level} (Ns : Set β„“) where ; Arrow = Mor ; πŸ™ = {!!} ; _βŠ•_ = {!!} - ; assoc = {!!} - ; ident = {!!} + ; isCategory = ? }