From 1bf565b87abeb96ebd29fce623633cf10a1a2982 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 5 Mar 2018 13:52:41 +0100 Subject: [PATCH] Have yoneda without having a category of categories I did break some things in Cat.Categories.Cat but since this is unprovable anyways it's not that big a deal. --- src/Cat/Categories/Cat.agda | 383 ++++++++++++++++-------------- src/Cat/Category/Exponential.agda | 42 ++-- src/Cat/Category/Monoid.agda | 15 +- src/Cat/Category/Product.agda | 28 ++- src/Cat/Category/Yoneda.agda | 16 +- 5 files changed, 259 insertions(+), 225 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index c7f1026..2bed7c2 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -11,7 +11,7 @@ open import Data.Product renaming (proj₁ to fst ; proj₂ to snd) open import Cat.Category open import Cat.Category.Functor open import Cat.Category.Product -open import Cat.Category.Exponential +open import Cat.Category.Exponential hiding (_×_ ; product) open import Cat.Category.NaturalTransformation open import Cat.Equality @@ -174,190 +174,211 @@ module _ {ℓ ℓ' : Level} (unprovable : IsCategory (RawCat ℓ ℓ')) where hasProducts = record { product = product } -- Basically proves that `Cat ℓ ℓ` is cartesian closed. +module CatExponential {ℓ : Level} (ℂ 𝔻 : Category ℓ ℓ) where + open Data.Product + open import Cat.Categories.Fun + + Categoryℓ = Category ℓ ℓ + open Fun ℂ 𝔻 renaming (identity to idN) + private + :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 + :func*: (F , A) = func* F A + + prodObj : Categoryℓ + prodObj = Fun + + module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where + private + F : Functor ℂ 𝔻 + F = proj₁ dom + A : Object ℂ + A = proj₂ dom + + G : Functor ℂ 𝔻 + G = proj₁ cod + B : Object ℂ + B = proj₂ cod + + :func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ]) + → 𝔻 [ func* F A , func* G B ] + :func→: ((θ , θNat) , f) = result + where + θA : 𝔻 [ func* F A , func* G A ] + θA = θ A + θB : 𝔻 [ func* F B , func* G B ] + θB = θ B + F→f : 𝔻 [ func* F A , func* F B ] + F→f = func→ F f + G→f : 𝔻 [ func* G A , func* G B ] + G→f = func→ G f + l : 𝔻 [ func* F A , func* G B ] + l = 𝔻 [ θB ∘ F→f ] + r : 𝔻 [ func* F A , func* G B ] + r = 𝔻 [ G→f ∘ θA ] + -- There are two choices at this point, + -- but I suppose the whole point is that + -- by `θNat f` we have `l ≡ r` + -- lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ] + -- lem = θNat f + result : 𝔻 [ func* F A , func* G B ] + result = l + + open CatProduct renaming (obj to _×p_) using () + + module _ {c : Functor ℂ 𝔻 × Object ℂ} where + private + F : Functor ℂ 𝔻 + F = proj₁ c + C : Object ℂ + C = proj₂ c + + -- NaturalTransformation F G × ℂ .Arrow A B + -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙 + -- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity) + -- where + -- open module 𝔻 = IsCategory (𝔻 .isCategory) + -- Unfortunately the equational version has some ambigous arguments. + + :ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 + :ident: = begin + :func→: {c} {c} (𝟙 (prodObj ×p ℂ) {c}) ≡⟨⟩ + :func→: {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ + 𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩ + 𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩ + func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩ + 𝟙 𝔻 ∎ + where + open module 𝔻 = Category 𝔻 + open module F = Functor F + + module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where + F = F×A .proj₁ + A = F×A .proj₂ + G = G×B .proj₁ + B = G×B .proj₂ + H = H×C .proj₁ + C = H×C .proj₂ + -- Not entirely clear what this is at this point: + _P⊕_ = Category._∘_ (prodObj ×p ℂ) {F×A} {G×B} {H×C} + module _ + -- NaturalTransformation F G × ℂ .Arrow A B + {θ×f : NaturalTransformation F G × ℂ [ A , B ]} + {η×g : NaturalTransformation G H × ℂ [ B , C ]} where + private + θ : Transformation F G + θ = proj₁ (proj₁ θ×f) + θNat : Natural F G θ + θNat = proj₂ (proj₁ θ×f) + f : ℂ [ A , B ] + f = proj₂ θ×f + η : Transformation G H + η = proj₁ (proj₁ η×g) + ηNat : Natural G H η + ηNat = proj₂ (proj₁ η×g) + g : ℂ [ B , C ] + g = proj₂ η×g + + ηθNT : NaturalTransformation F H + ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat) + + ηθ = proj₁ ηθNT + ηθNat = proj₂ ηθNT + + :isDistributive: : + 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] + ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] + :isDistributive: = begin + 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] + ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ + 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] + ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩ + 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] + ≡⟨ sym isAssociative ⟩ + 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) isAssociative ⟩ + 𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ func→ H f ∘ η A ] ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩ + 𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ η B ∘ func→ G f ] ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (sym isAssociative) ⟩ + 𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ] + ≡⟨ isAssociative ⟩ + 𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩ + 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] + ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩ + 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎ + where + open Category 𝔻 + module H = Functor H + + eval : Functor (CatProduct.obj prodObj ℂ) 𝔻 + -- :eval: : Functor (prodObj ×p ℂ) 𝔻 + eval = record + { raw = record + { func* = :func*: + ; func→ = λ {dom} {cod} → :func→: {dom} {cod} + } + ; isFunctor = record + { isIdentity = λ {o} → :ident: {o} + ; isDistributive = λ {f u n k y} → :isDistributive: {f} {u} {n} {k} {y} + } + } + + module _ (𝔸 : Category ℓ ℓ) (F : Functor (𝔸 ×p ℂ) 𝔻) where + -- open HasProducts (hasProducts {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct) + + postulate + parallelProduct + : Functor 𝔸 prodObj → Functor ℂ ℂ + → Functor (𝔸 ×p ℂ) (prodObj ×p ℂ) + transpose : Functor 𝔸 prodObj + eq : F[ eval ∘ (parallelProduct transpose (identity {C = ℂ})) ] ≡ F + -- eq : F[ :eval: ∘ {!!} ] ≡ F + -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F + -- eq' : (Catℓ [ :eval: ∘ + -- (record { product = product } HasProducts.|×| transpose) + -- (𝟙 Catℓ) + -- ]) + -- ≡ F + + -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758` + -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [ + -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose = + -- transpose , eq + module _ (ℓ : Level) (unprovable : IsCategory (RawCat ℓ ℓ)) where private - open Data.Product - open import Cat.Categories.Fun - Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ) Catℓ = Cat ℓ ℓ unprovable - module _ (ℂ 𝔻 : Category ℓ ℓ) where - open Fun ℂ 𝔻 renaming (identity to idN) - private - :obj: : Object Catℓ - :obj: = Fun + module _ (ℂ 𝔻 : Category ℓ ℓ) where + open CatExponential ℂ 𝔻 using (prodObj ; eval) + -- Putting in the type annotation causes Agda to loop indefinitely. + -- eval' : Functor (CatProduct.obj prodObj ℂ) 𝔻 + -- Likewise, using it below also results in this. + eval' : _ + eval' = eval + -- private + -- -- module _ (ℂ 𝔻 : Category ℓ ℓ) where + -- postulate :isExponential: : IsExponential Catℓ ℂ 𝔻 prodObj :eval: + -- -- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: + -- -- :isExponential: = {!catTranspose!} + -- -- where + -- -- open HasProducts (hasProducts {ℓ} {ℓ} unprovable) using (_|×|_) + -- -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F - :func*: : Functor ℂ 𝔻 × Object ℂ → Object 𝔻 - :func*: (F , A) = func* F A - - module _ {dom cod : Functor ℂ 𝔻 × Object ℂ} where - private - F : Functor ℂ 𝔻 - F = proj₁ dom - A : Object ℂ - A = proj₂ dom - - G : Functor ℂ 𝔻 - G = proj₁ cod - B : Object ℂ - B = proj₂ cod - - :func→: : (pobj : NaturalTransformation F G × ℂ [ A , B ]) - → 𝔻 [ func* F A , func* G B ] - :func→: ((θ , θNat) , f) = result - where - θA : 𝔻 [ func* F A , func* G A ] - θA = θ A - θB : 𝔻 [ func* F B , func* G B ] - θB = θ B - F→f : 𝔻 [ func* F A , func* F B ] - F→f = func→ F f - G→f : 𝔻 [ func* G A , func* G B ] - G→f = func→ G f - l : 𝔻 [ func* F A , func* G B ] - l = 𝔻 [ θB ∘ F→f ] - r : 𝔻 [ func* F A , func* G B ] - r = 𝔻 [ G→f ∘ θA ] - -- There are two choices at this point, - -- but I suppose the whole point is that - -- by `θNat f` we have `l ≡ r` - -- lem : 𝔻 [ θ B ∘ F .func→ f ] ≡ 𝔻 [ G .func→ f ∘ θ A ] - -- lem = θNat f - result : 𝔻 [ func* F A , func* G B ] - result = l - - _×p_ = product unprovable - - module _ {c : Functor ℂ 𝔻 × Object ℂ} where - private - F : Functor ℂ 𝔻 - F = proj₁ c - C : Object ℂ - C = proj₂ c - - -- NaturalTransformation F G × ℂ .Arrow A B - -- :ident: : :func→: {c} {c} (identityNat F , ℂ .𝟙) ≡ 𝔻 .𝟙 - -- :ident: = trans (proj₂ 𝔻.isIdentity) (F .isIdentity) - -- where - -- open module 𝔻 = IsCategory (𝔻 .isCategory) - -- Unfortunately the equational version has some ambigous arguments. - - :ident: : :func→: {c} {c} (NT.identity F , 𝟙 ℂ {A = proj₂ c}) ≡ 𝟙 𝔻 - :ident: = begin - :func→: {c} {c} (𝟙 (Product.obj (:obj: ×p ℂ)) {c}) ≡⟨⟩ - :func→: {c} {c} (idN F , 𝟙 ℂ) ≡⟨⟩ - 𝔻 [ identityTrans F C ∘ func→ F (𝟙 ℂ)] ≡⟨⟩ - 𝔻 [ 𝟙 𝔻 ∘ func→ F (𝟙 ℂ)] ≡⟨ proj₂ 𝔻.isIdentity ⟩ - func→ F (𝟙 ℂ) ≡⟨ F.isIdentity ⟩ - 𝟙 𝔻 ∎ - where - open module 𝔻 = Category 𝔻 - open module F = Functor F - - module _ {F×A G×B H×C : Functor ℂ 𝔻 × Object ℂ} where - F = F×A .proj₁ - A = F×A .proj₂ - G = G×B .proj₁ - B = G×B .proj₂ - H = H×C .proj₁ - C = H×C .proj₂ - -- Not entirely clear what this is at this point: - _P⊕_ = Category._∘_ (Product.obj (:obj: ×p ℂ)) {F×A} {G×B} {H×C} - module _ - -- NaturalTransformation F G × ℂ .Arrow A B - {θ×f : NaturalTransformation F G × ℂ [ A , B ]} - {η×g : NaturalTransformation G H × ℂ [ B , C ]} where - private - θ : Transformation F G - θ = proj₁ (proj₁ θ×f) - θNat : Natural F G θ - θNat = proj₂ (proj₁ θ×f) - f : ℂ [ A , B ] - f = proj₂ θ×f - η : Transformation G H - η = proj₁ (proj₁ η×g) - ηNat : Natural G H η - ηNat = proj₂ (proj₁ η×g) - g : ℂ [ B , C ] - g = proj₂ η×g - - ηθNT : NaturalTransformation F H - ηθNT = Category._∘_ Fun {F} {G} {H} (η , ηNat) (θ , θNat) - - ηθ = proj₁ ηθNT - ηθNat = proj₂ ηθNT - - :isDistributive: : - 𝔻 [ 𝔻 [ η C ∘ θ C ] ∘ func→ F ( ℂ [ g ∘ f ] ) ] - ≡ 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] - :isDistributive: = begin - 𝔻 [ (ηθ C) ∘ func→ F (ℂ [ g ∘ f ]) ] - ≡⟨ ηθNat (ℂ [ g ∘ f ]) ⟩ - 𝔻 [ func→ H (ℂ [ g ∘ f ]) ∘ (ηθ A) ] - ≡⟨ cong (λ φ → 𝔻 [ φ ∘ ηθ A ]) (H.isDistributive) ⟩ - 𝔻 [ 𝔻 [ func→ H g ∘ func→ H f ] ∘ (ηθ A) ] - ≡⟨ sym isAssociative ⟩ - 𝔻 [ func→ H g ∘ 𝔻 [ func→ H f ∘ ηθ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) isAssociative ⟩ - 𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ func→ H f ∘ η A ] ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (cong (λ φ → 𝔻 [ φ ∘ θ A ]) (sym (ηNat f))) ⟩ - 𝔻 [ func→ H g ∘ 𝔻 [ 𝔻 [ η B ∘ func→ G f ] ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ func→ H g ∘ φ ]) (sym isAssociative) ⟩ - 𝔻 [ func→ H g ∘ 𝔻 [ η B ∘ 𝔻 [ func→ G f ∘ θ A ] ] ] - ≡⟨ isAssociative ⟩ - 𝔻 [ 𝔻 [ func→ H g ∘ η B ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ φ ∘ 𝔻 [ func→ G f ∘ θ A ] ]) (sym (ηNat g)) ⟩ - 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ func→ G f ∘ θ A ] ] - ≡⟨ cong (λ φ → 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ φ ]) (sym (θNat f)) ⟩ - 𝔻 [ 𝔻 [ η C ∘ func→ G g ] ∘ 𝔻 [ θ B ∘ func→ F f ] ] ∎ - where - open Category 𝔻 - module H = Functor H - - :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 - :eval: = record - { raw = record - { func* = :func*: - ; func→ = λ {dom} {cod} → :func→: {dom} {cod} - } - ; isFunctor = record - { isIdentity = λ {o} → :ident: {o} - ; isDistributive = λ {f u n k y} → :isDistributive: {f} {u} {n} {k} {y} - } - } - - module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where - open HasProducts (hasProducts {ℓ} {ℓ} unprovable) renaming (_|×|_ to parallelProduct) - - postulate - transpose : Functor 𝔸 :obj: - eq : Catℓ [ :eval: ∘ (parallelProduct transpose (𝟙 Catℓ {A = ℂ})) ] ≡ F - -- eq : Catℓ [ :eval: ∘ (HasProducts._|×|_ hasProducts transpose (𝟙 Catℓ {o = ℂ})) ] ≡ F - -- eq' : (Catℓ [ :eval: ∘ - -- (record { product = product } HasProducts.|×| transpose) - -- (𝟙 Catℓ) - -- ]) - -- ≡ F - - -- For some reason after `e8215b2c051062c6301abc9b3f6ec67106259758` - -- `catTranspose` makes Agda hang. catTranspose : ∃![ F~ ] (Catℓ [ - -- :eval: ∘ (parallelProduct F~ (𝟙 Catℓ {o = ℂ}))] ≡ F) catTranspose = - -- transpose , eq - - postulate :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: - -- :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: - -- :isExponential: = {!catTranspose!} - -- where - -- open HasProducts (hasProducts {ℓ} {ℓ} unprovable) using (_|×|_) - -- :isExponential: = λ 𝔸 F → transpose 𝔸 F , eq' 𝔸 F - - -- :exponent: : Exponential (Cat ℓ ℓ) A B - :exponent: : Exponential Catℓ ℂ 𝔻 - :exponent: = record - { obj = :obj: - ; eval = :eval: - ; isExponential = :isExponential: - } + -- -- :exponent: : Exponential (Cat ℓ ℓ) A B + exponent : Exponential Catℓ ℂ 𝔻 + exponent = record + { obj = prodObj + ; eval = {!evalll'!} + ; isExponential = {!:isExponential:!} + } + where + open HasProducts (hasProducts unprovable) renaming (_×_ to _×p_) + open import Cat.Categories.Fun + open Fun + -- _×p_ = CatProduct.obj -- prodObj ℂ + -- eval' : Functor CatP.obj 𝔻 hasExponentials : HasExponentials Catℓ - hasExponentials = record { exponent = :exponent: } + hasExponentials = record { exponent = exponent } diff --git a/src/Cat/Category/Exponential.agda b/src/Cat/Category/Exponential.agda index 1e443ce..87769f6 100644 --- a/src/Cat/Category/Exponential.agda +++ b/src/Cat/Category/Exponential.agda @@ -1,40 +1,44 @@ module Cat.Category.Exponential where open import Agda.Primitive -open import Data.Product +open import Data.Product hiding (_×_) open import Cubical open import Cat.Category open import Cat.Category.Product -open Category - module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where - open HasProducts hasProducts - open Product hiding (obj) - private - _×p_ : (A B : Object ℂ) → Object ℂ - _×p_ A B = Product.obj (product A B) + open Category ℂ + open HasProducts hasProducts public - module _ (B C : Object ℂ) where - IsExponential : (Cᴮ : Object ℂ) → ℂ [ Cᴮ ×p B , C ] → Set (ℓ ⊔ ℓ') - IsExponential Cᴮ eval = ∀ (A : Object ℂ) (f : ℂ [ A ×p B , C ]) + module _ (B C : Object) where + record IsExponential' + (Cᴮ : Object) + (eval : ℂ [ Cᴮ × B , C ]) : Set (ℓ ⊔ ℓ') where + field + uniq + : ∀ (A : Object) (f : ℂ [ A × B , C ]) + → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f) + + IsExponential : (Cᴮ : Object) → ℂ [ Cᴮ × B , C ] → Set (ℓ ⊔ ℓ') + IsExponential Cᴮ eval = ∀ (A : Object) (f : ℂ [ A × B , C ]) → ∃![ f~ ] (ℂ [ eval ∘ f~ |×| Category.𝟙 ℂ ] ≡ f) record Exponential : Set (ℓ ⊔ ℓ') where field -- obj ≡ Cᴮ - obj : Object ℂ - eval : ℂ [ obj ×p B , C ] + obj : Object + eval : ℂ [ obj × B , C ] {{isExponential}} : IsExponential obj eval - -- If I make this an instance-argument then the instance resolution - -- algorithm goes into an infinite loop. Why? - exponentialsHaveProducts : HasProducts ℂ - exponentialsHaveProducts = hasProducts - transpose : (A : Object ℂ) → ℂ [ A ×p B , C ] → ℂ [ A , obj ] + + transpose : (A : Object) → ℂ [ A × B , C ] → ℂ [ A , obj ] transpose A f = proj₁ (isExponential A f) record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where + open Category ℂ open Exponential public field - exponent : (A B : Object ℂ) → Exponential ℂ A B + exponent : (A B : Object) → Exponential ℂ A B + + _⇑_ : (A B : Object) → Object + A ⇑ B = (exponent A B) .obj diff --git a/src/Cat/Category/Monoid.agda b/src/Cat/Category/Monoid.agda index 6cce193..a17468e 100644 --- a/src/Cat/Category/Monoid.agda +++ b/src/Cat/Category/Monoid.agda @@ -27,9 +27,10 @@ module _ (ℓa ℓb : Level) where open Category category public field {{hasProducts}} : HasProducts category - mempty : Object + empty : Object -- aka. tensor product, monoidal product. - mappend : Functor (category × category) category + append : Functor (category × category) category + open HasProducts hasProducts public record MonoidalCategory : Set ℓ where field @@ -40,10 +41,10 @@ module _ {ℓa ℓb : Level} (ℂ : MonoidalCategory ℓa ℓb) where private ℓ = ℓa ⊔ ℓb - module MC = MonoidalCategory ℂ - open HasProducts MC.hasProducts + open MonoidalCategory ℂ public + record Monoid : Set ℓ where field - carrier : MC.Object - mempty : MC.Arrow (carrier × carrier) carrier - mappend : MC.Arrow MC.mempty carrier + carrier : Object + mempty : Arrow empty carrier + mappend : Arrow (carrier × carrier) carrier diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda index 5eca0e0..aeb4f44 100644 --- a/src/Cat/Category/Product.agda +++ b/src/Cat/Category/Product.agda @@ -31,6 +31,7 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : Object ℂ) : proj₂ : ℂ [ obj , B ] {{isProduct}} : IsProduct ℂ proj₁ proj₂ + -- | Arrow product _P[_×_] : ∀ {X} → (π₁ : ℂ [ X , A ]) (π₂ : ℂ [ X , B ]) → ℂ [ X , obj ] _P[_×_] π₁ π₂ = proj₁ (isProduct π₁ π₂) @@ -39,16 +40,21 @@ record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ field product : ∀ (A B : Object ℂ) → Product {ℂ = ℂ} A B - open Product + open Product hiding (obj) - _×_ : (A B : Object ℂ) → Object ℂ - A × B = Product.obj (product A B) - -- The product mentioned in awodey in Def 6.1 is not the regular product of arrows. - -- It's a "parallel" product - _|×|_ : {A A' B B' : Object ℂ} → ℂ [ A , A' ] → ℂ [ B , B' ] - → ℂ [ A × B , A' × B' ] - _|×|_ {A = A} {A' = A'} {B = B} {B' = B'} a b - = product A' B' - P[ ℂ [ a ∘ (product A B) .proj₁ ] - × ℂ [ b ∘ (product A B) .proj₂ ] + module _ (A B : Object ℂ) where + open Product (product A B) + _×_ : Object ℂ + _×_ = obj + + -- | Parallel product of arrows + -- + -- The product mentioned in awodey in Def 6.1 is not the regular product of + -- arrows. It's a "parallel" product + module _ {A A' B B' : Object ℂ} where + open Product (product A B) hiding (_P[_×_]) renaming (proj₁ to fst ; proj₂ to snd) + _|×|_ : ℂ [ A , A' ] → ℂ [ B , B' ] → ℂ [ A × B , A' × B' ] + a |×| b = product A' B' + P[ ℂ [ a ∘ fst ] + × ℂ [ b ∘ snd ] ] diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda index df39252..365f441 100644 --- a/src/Cat/Category/Yoneda.agda +++ b/src/Cat/Category/Yoneda.agda @@ -15,7 +15,7 @@ open Equality.Data.Product -- category of categories (since it doesn't exist). open import Cat.Categories.Cat using (RawCat) -module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat ℓ ℓ)) where +module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where private open import Cat.Categories.Fun open import Cat.Categories.Sets @@ -24,15 +24,17 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat open Functor 𝓢 = Sets ℓ open Fun (opposite ℂ) 𝓢 - Catℓ : Category _ _ - Catℓ = Cat.Cat ℓ ℓ unprovable prshf = presheaf ℂ module ℂ = Category ℂ - _⇑_ : (A B : Category.Object Catℓ) → Category.Object Catℓ - A ⇑ B = (exponent A B) .obj - where - open HasExponentials (Cat.hasExponentials ℓ unprovable) + -- There is no (small) category of categories. So we won't use _⇑_ from + -- `HasExponential` + -- + -- open HasExponentials (Cat.hasExponentials ℓ unprovable) using (_⇑_) + -- + -- In stead we'll use an ad-hoc definition -- which is definitionally + -- equivalent to that other one. + _⇑_ = Cat.CatExponential.prodObj module _ {A B : ℂ.Object} (f : ℂ [ A , B ]) where :func→: : NaturalTransformation (prshf A) (prshf B)