diff --git a/src/Cat.agda b/src/Cat.agda index f7c744e..0619b51 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -7,12 +7,14 @@ import Cat.Category.Functor import Cat.Category.Product import Cat.Category.Exponential import Cat.Category.CartesianClosed +import Cat.Category.NaturalTransformation import Cat.Category.Pathy import Cat.Category.Bij import Cat.Category.Properties +import Cat.Category.Monad import Cat.Categories.Sets --- import Cat.Categories.Cat +import Cat.Categories.Cat import Cat.Categories.Rel import Cat.Categories.Free import Cat.Categories.Fun diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index b7e306e..2bb566e 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -12,6 +12,7 @@ open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product open import Cat.Category.Exponential +open import Cat.Category.NaturalTransformation open import Cat.Equality open Equality.Data.Product @@ -176,9 +177,10 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ) Catℓ = Cat ℓ ℓ unprovable module _ (ℂ 𝔻 : Category ℓ ℓ) where + open Fun ℂ 𝔻 renaming (identity to idN) private :obj: : Object Catℓ - :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻} + :obj: = Fun :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 :func*: (F , A) = func* F A @@ -234,10 +236,11 @@ module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where -- where -- open module 𝔻 = IsCategory (𝔻 .isCategory) -- Unfortunately the equational version has some ambigous arguments. - :ident: : :func→: {c} {c} (identityNat F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 + + :ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 :ident: = begin :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩ - :func→: {c} {c} (identityNat F , 𝟙 ℂ) ≡⟨⟩ + :func→: {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ 𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩ 𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩ func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩ diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 3e4dcbf..70dab6c 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -2,99 +2,29 @@ module Cat.Categories.Fun where open import Agda.Primitive -open import Cubical -open import Function open import Data.Product -import Cubical.GradLemma -module UIP = Cubical.GradLemma -open import Cubical.Sigma -open import Cubical.NType -open import Cubical.NType.Properties + open import Data.Nat using (_≤_ ; z≤n ; s≤s) module Nat = Data.Nat +open import Data.Product + +open import Cubical +open import Cubical.Sigma +open import Cubical.NType.Properties open import Cat.Category -open import Cat.Category.Functor +open import Cat.Category.Functor hiding (identity) +open import Cat.Category.NaturalTransformation open import Cat.Wishlist open import Cat.Equality +import Cat.Category.NaturalTransformation open Equality.Data.Product -module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where +module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where open Category using (Object ; 𝟙) - open Functor - - module _ (F G : Functor ℂ 𝔻) where - private - module F = Functor F - module G = Functor G - -- What do you call a non-natural tranformation? - Transformation : Set (ℓc ⊔ ℓd') - Transformation = (C : Object ℂ) → 𝔻 [ F.func* C , G.func* C ] - - Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd')) - Natural θ - = {A B : Object ℂ} - → (f : ℂ [ A , B ]) - → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ] - - NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') - NaturalTransformation = Σ Transformation Natural - - -- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd')) - -- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A) - - NaturalTransformation≡ : {α β : NaturalTransformation} - → (eq₁ : α .proj₁ ≡ β .proj₁) - → (eq₂ : PathP - (λ i → {A B : Object ℂ} (f : ℂ [ A , B ]) - → 𝔻 [ eq₁ i B ∘ F.func→ f ] - ≡ 𝔻 [ G.func→ f ∘ eq₁ i A ]) - (α .proj₂) (β .proj₂)) - → α ≡ β - NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i - - identityTrans : (F : Functor ℂ 𝔻) → Transformation F F - identityTrans F C = 𝟙 𝔻 - - identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F) - identityNatural F {A = A} {B = B} f = begin - 𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩ - F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩ - 𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩ - 𝔻 [ F→ f ∘ identityTrans F A ] ∎ - where - module F = Functor F - F→ = F.func→ - module 𝔻 = Category 𝔻 - - identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F - identityNat F = identityTrans F , identityNatural F - - module _ {F G H : Functor ℂ 𝔻} where - private - module F = Functor F - module G = Functor G - module H = Functor H - _∘nt_ : Transformation G H → Transformation F G → Transformation F H - (θ ∘nt η) C = 𝔻 [ θ C ∘ η C ] - - NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H - proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η - proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin - 𝔻 [ (θ ∘nt η) B ∘ F.func→ f ] ≡⟨⟩ - 𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym isAssociative ⟩ - 𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩ - 𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ isAssociative ⟩ - 𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩ - 𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym isAssociative ⟩ - 𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩ - 𝔻 [ H.func→ f ∘ (θ ∘nt η) A ] ∎ - where - open Category 𝔻 - - NatComp = _:⊕:_ + module NT = NaturalTransformation ℂ 𝔻 + open NT public private module 𝔻 = Category 𝔻 @@ -147,21 +77,20 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat f' C ∎ eq-l : ∀ C → (𝔻 [ identityTrans B C ∘ f' C ]) ≡ f' C eq-l C = proj₂ 𝔻.isIdentity - ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f + ident-r : (_:⊕:_ {A} {A} {B} f (NT.identity A)) ≡ f ident-r = lemSig allNatural _ _ (funExt eq-r) - ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f + ident-l : (_:⊕:_ {A} {B} {B} (NT.identity B) f) ≡ f ident-l = lemSig allNatural _ _ (funExt eq-l) - :ident: - : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f - × (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f - :ident: = ident-r , ident-l - + isIdentity + : (_:⊕:_ {A} {A} {B} f (NT.identity A)) ≡ f + × (_:⊕:_ {A} {B} {B} (NT.identity B) f) ≡ f + isIdentity = ident-r , ident-l -- Functor categories. Objects are functors, arrows are natural transformations. RawFun : RawCategory (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd') RawFun = record { Object = Functor ℂ 𝔻 ; Arrow = NaturalTransformation - ; 𝟙 = λ {F} → identityNat F + ; 𝟙 = λ {F} → NT.identity F ; _∘_ = λ {F G H} → _:⊕:_ {F} {G} {H} } @@ -169,7 +98,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat :isCategory: : IsCategory RawFun :isCategory: = record { isAssociative = λ {A B C D} → :isAssociative: {A} {B} {C} {D} - ; isIdentity = λ {A B} → :ident: {A} {B} + ; isIdentity = λ {A B} → isIdentity {A} {B} ; arrowsAreSets = λ {F} {G} → naturalTransformationIsSets {F} {G} ; univalent = {!!} } @@ -179,12 +108,13 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where open import Cat.Categories.Sets + open NaturalTransformation (Opposite ℂ) (𝓢𝓮𝓽 ℓ') -- Restrict the functors to Presheafs. RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ') RawPresh = record { Object = Presheaf ℂ ; Arrow = NaturalTransformation - ; 𝟙 = λ {F} → identityNat F + ; 𝟙 = λ {F} → identity F ; _∘_ = λ {F G H} → NatComp {F = F} {G = G} {H = H} } diff --git a/src/Cat/Category/Monad.agda b/src/Cat/Category/Monad.agda new file mode 100644 index 0000000..6c73f06 --- /dev/null +++ b/src/Cat/Category/Monad.agda @@ -0,0 +1,8 @@ +{-# OPTIONS --cubical #-} +module Cat.Category.Monad where + +open import Cubical + +open import Cat.Category +open import Cat.Category.Functor +open import Cat.Categories.Fun diff --git a/src/Cat/Category/NaturalTransformation.agda b/src/Cat/Category/NaturalTransformation.agda new file mode 100644 index 0000000..b56694c --- /dev/null +++ b/src/Cat/Category/NaturalTransformation.agda @@ -0,0 +1,82 @@ +{-# OPTIONS --allow-unsolved-metas --cubical #-} +module Cat.Category.NaturalTransformation where +open import Agda.Primitive +open import Data.Product + +open import Cubical + +open import Cat.Category +open import Cat.Category.Functor hiding (identity) + +module NaturalTransformation {ℓc ℓc' ℓd ℓd' : Level} + (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where + open Category using (Object ; 𝟙) + + module _ (F G : Functor ℂ 𝔻) where + private + module F = Functor F + module G = Functor G + -- What do you call a non-natural tranformation? + Transformation : Set (ℓc ⊔ ℓd') + Transformation = (C : Object ℂ) → 𝔻 [ F.func* C , G.func* C ] + + Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd')) + Natural θ + = {A B : Object ℂ} + → (f : ℂ [ A , B ]) + → 𝔻 [ θ B ∘ F.func→ f ] ≡ 𝔻 [ G.func→ f ∘ θ A ] + + NaturalTransformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') + NaturalTransformation = Σ Transformation Natural + + NaturalTransformation≡ : {α β : NaturalTransformation} + → (eq₁ : α .proj₁ ≡ β .proj₁) + → (eq₂ : PathP + (λ i → {A B : Object ℂ} (f : ℂ [ A , B ]) + → 𝔻 [ eq₁ i B ∘ F.func→ f ] + ≡ 𝔻 [ G.func→ f ∘ eq₁ i A ]) + (α .proj₂) (β .proj₂)) + → α ≡ β + NaturalTransformation≡ eq₁ eq₂ i = eq₁ i , eq₂ i + + identityTrans : (F : Functor ℂ 𝔻) → Transformation F F + identityTrans F C = 𝟙 𝔻 + + identityNatural : (F : Functor ℂ 𝔻) → Natural F F (identityTrans F) + identityNatural F {A = A} {B = B} f = begin + 𝔻 [ identityTrans F B ∘ F→ f ] ≡⟨⟩ + 𝔻 [ 𝟙 𝔻 ∘ F→ f ] ≡⟨ proj₂ 𝔻.isIdentity ⟩ + F→ f ≡⟨ sym (proj₁ 𝔻.isIdentity) ⟩ + 𝔻 [ F→ f ∘ 𝟙 𝔻 ] ≡⟨⟩ + 𝔻 [ F→ f ∘ identityTrans F A ] ∎ + where + module F = Functor F + F→ = F.func→ + module 𝔻 = Category 𝔻 + + identity : (F : Functor ℂ 𝔻) → NaturalTransformation F F + identity F = identityTrans F , identityNatural F + + module _ {F G H : Functor ℂ 𝔻} where + private + module F = Functor F + module G = Functor G + module H = Functor H + _∘nt_ : Transformation G H → Transformation F G → Transformation F H + (θ ∘nt η) C = 𝔻 [ θ C ∘ η C ] + + NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H + proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η + proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin + 𝔻 [ (θ ∘nt η) B ∘ F.func→ f ] ≡⟨⟩ + 𝔻 [ 𝔻 [ θ B ∘ η B ] ∘ F.func→ f ] ≡⟨ sym isAssociative ⟩ + 𝔻 [ θ B ∘ 𝔻 [ η B ∘ F.func→ f ] ] ≡⟨ cong (λ φ → 𝔻 [ θ B ∘ φ ]) (ηNat f) ⟩ + 𝔻 [ θ B ∘ 𝔻 [ G.func→ f ∘ η A ] ] ≡⟨ isAssociative ⟩ + 𝔻 [ 𝔻 [ θ B ∘ G.func→ f ] ∘ η A ] ≡⟨ cong (λ φ → 𝔻 [ φ ∘ η A ]) (θNat f) ⟩ + 𝔻 [ 𝔻 [ H.func→ f ∘ θ A ] ∘ η A ] ≡⟨ sym isAssociative ⟩ + 𝔻 [ H.func→ f ∘ 𝔻 [ θ A ∘ η A ] ] ≡⟨⟩ + 𝔻 [ H.func→ f ∘ (θ ∘nt η) A ] ∎ + where + open Category 𝔻 + + NatComp = _:⊕:_ diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 190592e..4eeb6c3 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -52,6 +52,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat open import Cat.Category.Exponential open Functor 𝓢 = Sets ℓ + open Fun (Opposite ℂ) 𝓢 private Catℓ : Category _ _ Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable} @@ -80,7 +81,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat eq : (λ C x → ℂ [ ℂ.𝟙 ∘ x ]) ≡ identityTrans (prshf c) eq = funExt λ A → funExt λ B → proj₂ ℂ.isIdentity - yoneda : Functor ℂ (Fun {ℂ = Opposite ℂ} {𝔻 = 𝓢}) + yoneda : Functor ℂ Fun yoneda = record { raw = record { func* = prshf