diff --git a/src/Cat.agda b/src/Cat.agda index d6a24c0..4cb7bb8 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -8,7 +8,7 @@ import Cat.Category.Bij import Cat.Category.Free import Cat.Category.Properties import Cat.Categories.Sets -import Cat.Categories.Cat +-- import Cat.Categories.Cat import Cat.Categories.Rel import Cat.Categories.Fun import Cat.Categories.Cube diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 9d4af34..0fe0056 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -1,3 +1,4 @@ +-- There is no category of categories in our interpretation {-# OPTIONS --cubical --allow-unsolved-metas #-} module Cat.Categories.Cat where diff --git a/src/Cat/Categories/Rel.agda b/src/Cat/Categories/Rel.agda index 43f3409..7d7eeb8 100644 --- a/src/Cat/Categories/Rel.agda +++ b/src/Cat/Categories/Rel.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical #-} +{-# OPTIONS --cubical --allow-unsolved-metas #-} module Cat.Categories.Rel where open import Cubical @@ -160,5 +160,10 @@ 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 )} - ; isCategory = record { assoc = funExt is-assoc ; ident = funExt ident-l , funExt ident-r } + ; isCategory = record + { assoc = funExt is-assoc + ; ident = funExt ident-l , funExt ident-r + ; arrow-is-set = {!!} + ; univalent = {!!} + } } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 31a0b63..bf5744b 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} module Cat.Categories.Sets where open import Cubical diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index e4c39a9..8a320f1 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --cubical #-} +{-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Category where @@ -22,23 +22,65 @@ open import Cubical syntax βˆƒ!-syntax (Ξ» x β†’ B) = βˆƒ![ x ] B --- All projections must be `isProp`'s +-- Thierry: All projections must be `isProp`'s + +-- According to definitions 9.1.1 and 9.1.6 in the HoTT book the +-- arrows of a category form a set (arrow-is-set), and there is an +-- equivalence between the equality of objects and isomorphisms +-- (univalent). 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) + (_∘_ : { 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 + β†’ h ∘ (g ∘ f) ≑ (h ∘ g) ∘ f ident : {A B : Object} {f : Arrow A B} - β†’ f βŠ• πŸ™ ≑ f Γ— πŸ™ βŠ• f ≑ f + β†’ f ∘ πŸ™ ≑ f Γ— πŸ™ ∘ f ≑ f + arrow-is-set : βˆ€ {A B : Object} β†’ isSet (Arrow A B) + + Isomorphism : βˆ€ {A B} β†’ (f : Arrow A B) β†’ Set β„“' + Isomorphism {A} {B} f = Ξ£[ g ∈ Arrow B A ] g ∘ f ≑ πŸ™ Γ— f ∘ g ≑ πŸ™ + + _β‰…_ : (A B : Object) β†’ Set β„“' + _β‰…_ A B = Ξ£[ f ∈ Arrow A B ] (Isomorphism f) + + idIso : (A : Object) β†’ A β‰… A + idIso A = πŸ™ , (πŸ™ , ident) + + 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. + field + univalent : {A B : Object} β†’ isEquiv (A ≑ B) (A β‰… B) (id-to-iso A B) + + module _ {A B : Object} where + Epimorphism : {X : Object } β†’ (f : Arrow A B) β†’ Set β„“' + Epimorphism {X} f = ( gβ‚€ g₁ : Arrow B X ) β†’ gβ‚€ ∘ f ≑ g₁ ∘ f β†’ gβ‚€ ≑ g₁ + + Monomorphism : {X : Object} β†’ (f : Arrow A B) β†’ Set β„“' + Monomorphism {X} f = ( gβ‚€ g₁ : Arrow X A ) β†’ f ∘ gβ‚€ ≑ f ∘ g₁ β†’ gβ‚€ ≑ g₁ + +module _ {β„“} {β„“'} {Object : Set β„“} + {Arrow : Object β†’ Object β†’ Set β„“'} + {πŸ™ : {o : Object} β†’ Arrow o o} + {_βŠ•_ : { a b c : Object } β†’ Arrow b c β†’ Arrow a b β†’ Arrow a c} + where + + -- TODO, provable by using arrow-is-set and that isProp (isEquiv _ _ _) + -- This lemma will be useful to prove the equality of two categories. + IsCategory-is-prop : isProp (IsCategory Object Arrow πŸ™ _βŠ•_) + IsCategory-is-prop = {!!} --- open IsCategory public record Category (β„“ β„“' : Level) : Set (lsuc (β„“' βŠ” β„“)) where -- adding no-eta-equality can speed up type-checking. + -- ONLY IF you define your categories with copatterns though. no-eta-equality field -- Need something like: @@ -64,23 +106,6 @@ _[_,_] = Arrow _[_∘_] : βˆ€ {β„“ β„“'} β†’ (β„‚ : Category β„“ β„“') β†’ {A B C : β„‚ .Object} β†’ (g : β„‚ [ B , C ]) β†’ (f : β„‚ [ A , B ]) β†’ β„‚ [ A , C ] _[_∘_] = _∘_ - - -module _ {β„“ β„“' : Level} {β„‚ : Category β„“ β„“'} where - module _ { A B : β„‚ .Object } where - Isomorphism : (f : β„‚ .Arrow A B) β†’ Set β„“' - Isomorphism f = Ξ£[ g ∈ β„‚ .Arrow B A ] β„‚ [ g ∘ f ] ≑ β„‚ .πŸ™ Γ— β„‚ [ f ∘ g ] ≑ β„‚ .πŸ™ - - Epimorphism : {X : β„‚ .Object } β†’ (f : β„‚ .Arrow A B) β†’ Set β„“' - Epimorphism {X} f = ( gβ‚€ g₁ : β„‚ .Arrow B X ) β†’ β„‚ [ gβ‚€ ∘ f ] ≑ β„‚ [ g₁ ∘ f ] β†’ gβ‚€ ≑ g₁ - - Monomorphism : {X : β„‚ .Object} β†’ (f : β„‚ .Arrow A B) β†’ Set β„“' - Monomorphism {X} f = ( gβ‚€ g₁ : β„‚ .Arrow X A ) β†’ β„‚ [ f ∘ gβ‚€ ] ≑ β„‚ [ f ∘ g₁ ] β†’ gβ‚€ ≑ g₁ - - -- Isomorphism of objects - _β‰…_ : (A B : Object β„‚) β†’ Set β„“' - _β‰…_ A B = Ξ£[ f ∈ β„‚ .Arrow A B ] (Isomorphism f) - module _ {β„“ β„“' : Level} (β„‚ : Category β„“ β„“') {A B obj : Object β„‚} where IsProduct : (π₁ : Arrow β„‚ obj A) (Ο€β‚‚ : Arrow β„‚ obj B) β†’ Set (β„“ βŠ” β„“') IsProduct π₁ Ο€β‚‚ @@ -130,7 +155,9 @@ module _ {β„“ β„“' : Level} (β„‚ : Category β„“ β„“') where ; Arrow = Function.flip (β„‚ .Arrow) ; πŸ™ = β„‚ .πŸ™ ; _∘_ = Function.flip (β„‚ ._∘_) - ; isCategory = record { assoc = sym assoc ; ident = swap ident } + ; isCategory = record { assoc = sym assoc ; ident = swap ident + ; arrow-is-set = {!!} + ; univalent = {!!} } } where open IsCategory (β„‚ .isCategory) diff --git a/src/Cat/Category/Free.agda b/src/Cat/Category/Free.agda index 1facb03..4d5db54 100644 --- a/src/Cat/Category/Free.agda +++ b/src/Cat/Category/Free.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} module Cat.Category.Free where open import Agda.Primitive @@ -32,5 +33,10 @@ module _ {β„“ β„“' : Level} (β„‚ : Category β„“ β„“') where ; Arrow = Path ; πŸ™ = Ξ» {o} β†’ emptyPath o ; _∘_ = Ξ» {a b c} β†’ concatenate {a} {b} {c} - ; isCategory = record { assoc = p-assoc ; ident = ident-r , ident-l } + ; isCategory = record + { assoc = p-assoc + ; ident = ident-r , ident-l + ; arrow-is-set = {!!} + ; univalent = {!!} + } } diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 8ef3026..20631e4 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -16,7 +16,7 @@ module _ {β„“ β„“' : Level} {β„‚ : Category β„“ β„“'} { A B : β„‚ .Category.Obje open Category β„‚ open IsCategory (isCategory) - iso-is-epi : Isomorphism {β„‚ = β„‚} f β†’ Epimorphism {β„‚ = β„‚} {X = X} f + iso-is-epi : Isomorphism f β†’ Epimorphism {X = X} f iso-is-epi (f- , left-inv , right-inv) gβ‚€ g₁ eq = begin gβ‚€ β‰‘βŸ¨ sym (proj₁ ident) ⟩ gβ‚€ ∘ πŸ™ β‰‘βŸ¨ cong (_∘_ gβ‚€) (sym right-inv) ⟩ @@ -27,7 +27,7 @@ module _ {β„“ β„“' : Level} {β„‚ : Category β„“ β„“'} { A B : β„‚ .Category.Obje g₁ ∘ πŸ™ β‰‘βŸ¨ proj₁ ident ⟩ g₁ ∎ - iso-is-mono : Isomorphism {β„‚ = β„‚} f β†’ Monomorphism {β„‚ = β„‚} {X = X} f + iso-is-mono : Isomorphism f β†’ Monomorphism {X = X} f iso-is-mono (f- , (left-inv , right-inv)) gβ‚€ g₁ eq = begin gβ‚€ β‰‘βŸ¨ sym (projβ‚‚ ident) ⟩ @@ -39,7 +39,7 @@ module _ {β„“ β„“' : Level} {β„‚ : Category β„“ β„“'} { A B : β„‚ .Category.Obje πŸ™ ∘ g₁ β‰‘βŸ¨ projβ‚‚ ident ⟩ g₁ ∎ - iso-is-epi-mono : Isomorphism {β„‚ = β„‚} f β†’ Epimorphism {β„‚ = β„‚} {X = X} f Γ— Monomorphism {β„‚ = β„‚} {X = X} f + 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 {- @@ -54,71 +54,71 @@ open Category open import Cat.Functor open Functor -module _ {β„“ : Level} {β„‚ : Category β„“ β„“} - {isSObj : isSet (β„‚ .Object)} - {isz2 : βˆ€ {β„“} β†’ {A B : Set β„“} β†’ isSet (Sets [ A , B ])} where - open import Cat.Categories.Cat using (Cat) - open import Cat.Categories.Fun - open import Cat.Categories.Sets - module Cat = Cat.Categories.Cat - open Exponential - private - Catβ„“ = Cat β„“ β„“ - prshf = presheaf {β„‚ = β„‚} - module β„‚ = IsCategory (β„‚ .isCategory) +-- module _ {β„“ : Level} {β„‚ : Category β„“ β„“} +-- {isSObj : isSet (β„‚ .Object)} +-- {isz2 : βˆ€ {β„“} β†’ {A B : Set β„“} β†’ isSet (Sets [ A , B ])} where +-- -- open import Cat.Categories.Cat using (Cat) +-- open import Cat.Categories.Fun +-- open import Cat.Categories.Sets +-- -- module Cat = Cat.Categories.Cat +-- open Exponential +-- private +-- Catβ„“ = Cat β„“ β„“ +-- prshf = presheaf {β„‚ = β„‚} +-- module β„‚ = IsCategory (β„‚ .isCategory) - -- Exp : Set (lsuc (lsuc β„“)) - -- Exp = Exponential (Cat (lsuc β„“) β„“) - -- Sets (Opposite β„‚) +-- -- Exp : Set (lsuc (lsuc β„“)) +-- -- Exp = Exponential (Cat (lsuc β„“) β„“) +-- -- Sets (Opposite β„‚) - _⇑_ : (A B : Catβ„“ .Object) β†’ Catβ„“ .Object - A ⇑ B = (exponent A B) .obj - where - open HasExponentials (Cat.hasExponentials β„“) +-- _⇑_ : (A B : Catβ„“ .Object) β†’ Catβ„“ .Object +-- A ⇑ B = (exponent A B) .obj +-- where +-- open HasExponentials (Cat.hasExponentials β„“) - module _ {A B : β„‚ .Object} (f : β„‚ .Arrow A B) where - :funcβ†’: : NaturalTransformation (prshf A) (prshf B) - :funcβ†’: = (Ξ» C x β†’ β„‚ [ f ∘ x ]) , Ξ» f₁ β†’ funExt Ξ» _ β†’ β„‚.assoc +-- module _ {A B : β„‚ .Object} (f : β„‚ .Arrow A B) where +-- :funcβ†’: : NaturalTransformation (prshf A) (prshf B) +-- :funcβ†’: = (Ξ» C x β†’ β„‚ [ f ∘ x ]) , Ξ» f₁ β†’ funExt Ξ» _ β†’ β„‚.assoc - module _ {c : β„‚ .Object} where - eqTrans : (Ξ» _ β†’ Transformation (prshf c) (prshf c)) - [ (Ξ» _ x β†’ β„‚ [ β„‚ .πŸ™ ∘ x ]) ≑ identityTrans (prshf c) ] - eqTrans = funExt Ξ» x β†’ funExt Ξ» x β†’ β„‚.ident .projβ‚‚ +-- module _ {c : β„‚ .Object} where +-- eqTrans : (Ξ» _ β†’ Transformation (prshf c) (prshf c)) +-- [ (Ξ» _ x β†’ β„‚ [ β„‚ .πŸ™ ∘ x ]) ≑ identityTrans (prshf c) ] +-- eqTrans = funExt Ξ» x β†’ funExt Ξ» x β†’ β„‚.ident .projβ‚‚ - eqNat : (Ξ» i β†’ Natural (prshf c) (prshf c) (eqTrans i)) - [(Ξ» _ β†’ funExt (Ξ» _ β†’ β„‚.assoc)) ≑ identityNatural (prshf c)] - eqNat = Ξ» i {A} {B} f β†’ - let - open IsCategory (Sets .isCategory) - lemm : (Sets [ eqTrans i B ∘ prshf c .funcβ†’ f ]) ≑ - (Sets [ prshf c .funcβ†’ f ∘ eqTrans i A ]) - lemm = {!!} - lem : (Ξ» _ β†’ Sets [ Functor.func* (prshf c) A , prshf c .func* B ]) - [ Sets [ eqTrans i B ∘ prshf c .funcβ†’ f ] - ≑ Sets [ prshf c .funcβ†’ f ∘ eqTrans i A ] ] - lem - = isz2 _ _ lemm _ i - -- (Sets [ eqTrans i B ∘ prshf c .funcβ†’ f ]) - -- (Sets [ prshf c .funcβ†’ f ∘ eqTrans i A ]) - -- lemm - -- _ i - in - lem - -- eqNat = Ξ» {A} {B} i β„‚[B,A] i' β„‚[A,c] β†’ - -- let - -- k : β„‚ [ {!!} , {!!} ] - -- k = β„‚[A,c] - -- in {!β„‚ [ ? ∘ ? ]!} +-- eqNat : (Ξ» i β†’ Natural (prshf c) (prshf c) (eqTrans i)) +-- [(Ξ» _ β†’ funExt (Ξ» _ β†’ β„‚.assoc)) ≑ identityNatural (prshf c)] +-- eqNat = Ξ» i {A} {B} f β†’ +-- let +-- open IsCategory (Sets .isCategory) +-- lemm : (Sets [ eqTrans i B ∘ prshf c .funcβ†’ f ]) ≑ +-- (Sets [ prshf c .funcβ†’ f ∘ eqTrans i A ]) +-- lemm = {!!} +-- lem : (Ξ» _ β†’ Sets [ Functor.func* (prshf c) A , prshf c .func* B ]) +-- [ Sets [ eqTrans i B ∘ prshf c .funcβ†’ f ] +-- ≑ Sets [ prshf c .funcβ†’ f ∘ eqTrans i A ] ] +-- lem +-- = isz2 _ _ lemm _ i +-- -- (Sets [ eqTrans i B ∘ prshf c .funcβ†’ f ]) +-- -- (Sets [ prshf c .funcβ†’ f ∘ eqTrans i A ]) +-- -- lemm +-- -- _ i +-- in +-- lem +-- -- eqNat = Ξ» {A} {B} i β„‚[B,A] i' β„‚[A,c] β†’ +-- -- let +-- -- k : β„‚ [ {!!} , {!!} ] +-- -- k = β„‚[A,c] +-- -- in {!β„‚ [ ? ∘ ? ]!} - :ident: : (:funcβ†’: (β„‚ .πŸ™ {c})) ≑ (Fun .πŸ™ {o = prshf c}) - :ident: = Σ≑ eqTrans eqNat +-- :ident: : (:funcβ†’: (β„‚ .πŸ™ {c})) ≑ (Fun .πŸ™ {o = prshf c}) +-- :ident: = Σ≑ eqTrans eqNat - yoneda : Functor β„‚ (Fun {β„‚ = Opposite β„‚} {𝔻 = Sets {β„“}}) - yoneda = record - { func* = prshf - ; funcβ†’ = :funcβ†’: - ; isFunctor = record - { ident = :ident: - ; distrib = {!!} - } - } +-- yoneda : Functor β„‚ (Fun {β„‚ = Opposite β„‚} {𝔻 = Sets {β„“}}) +-- yoneda = record +-- { func* = prshf +-- ; funcβ†’ = :funcβ†’: +-- ; isFunctor = record +-- { ident = :ident: +-- ; distrib = {!!} +-- } +-- }