From c5a3673d9beb5a3b9a6b10f22131c4f1257b726d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Wed, 24 Jan 2018 16:38:28 +0100 Subject: [PATCH] Prove that Cat is cartesian closed WIP --- src/Cat/Categories/Cat.agda | 327 +++++++++++++++++++++++++------ src/Cat/Categories/Fun.agda | 2 +- src/Cat/Categories/Sets.agda | 39 +++- src/Cat/Category.agda | 47 +++++ src/Cat/Category/Properties.agda | 46 ++--- 5 files changed, 359 insertions(+), 102 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 796379b..61769b3 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -40,7 +40,7 @@ module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where lift-eq-functors eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; ident = eqI i ; distrib = eqD i } -- The category of categories -module _ {ℓ ℓ' : Level} where +module _ (ℓ ℓ' : Level) where private module _ {A B C D : Category ℓ ℓ'} {f : Functor A B} {g : Functor B C} {h : Functor C D} where eq* : func* (h ∘f (g ∘f f)) ≡ func* ((h ∘f g) ∘f f) @@ -94,81 +94,280 @@ module _ {ℓ ℓ' : Level} where } } -module _ {ℓ : Level} (C D : Category ℓ ℓ) where - private - :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} +module _ {ℓ ℓ' : Level} where + Catt = Cat ℓ ℓ' - 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) + module _ (C D : Category ℓ ℓ') where + private + :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: + ; 𝟙 = :𝟙: + ; _⊕_ = _:⊕:_ } - where - open module C = IsCategory (C .isCategory) - open module D = IsCategory (D .isCategory) - :product: : Category ℓ ℓ - :product: = record - { Object = :Object: - ; Arrow = :Arrow: - ; 𝟙 = :𝟙: - ; _⊕_ = _:⊕:_ + proj₁ : Arrow Catt :product: C + proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl } + + proj₂ : Arrow Catt :product: D + proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl } + + module _ {X : Object Catt} (x₁ : Arrow Catt X C) (x₂ : Arrow Catt X D) where + open Functor + + -- 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 :product: + x = record + { func* = λ x → (func* x₁) x , (func* x₂) x + ; func→ = λ x → func→ x₁ x , func→ x₂ x + ; ident = lift-eq (ident x₁) (ident x₂) + ; distrib = lift-eq (distrib x₁) (distrib x₂) + } + + -- Need to "lift equality of functors" + -- If I want to do this like I do it for pairs it's gonna be a pain. + postulate isUniqL : (Catt ⊕ proj₁) x ≡ x₁ + -- isUniqL = lift-eq-functors refl refl {!!} {!!} + + postulate isUniqR : (Catt ⊕ proj₂) x ≡ x₂ + -- isUniqR = lift-eq-functors refl refl {!!} {!!} + + isUniq : (Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂ + isUniq = isUniqL , isUniqR + + uniq : ∃![ x ] ((Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂) + uniq = x , isUniq + + instance + isProduct : IsProduct Catt proj₁ proj₂ + isProduct = uniq + + product : Product {ℂ = Catt} C D + product = record + { obj = :product: + ; proj₁ = proj₁ + ; proj₂ = proj₂ } - proj₁ : Arrow Cat :product: C - proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl } +module _ {ℓ ℓ' : Level} where + open Category + instance + CatHasProducts : HasProducts (Cat ℓ ℓ') + CatHasProducts = record { product = product } - proj₂ : Arrow Cat :product: D - proj₂ = record { func* = snd ; func→ = snd ; ident = refl ; distrib = refl } +-- Basically proves that `Cat ℓ ℓ` is cartesian closed. +module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ)}} where + open Data.Product + open Category - module _ {X : Object (Cat {ℓ} {ℓ})} (x₁ : Arrow Cat X C) (x₂ : Arrow Cat X D) where - open Functor + private + Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ) + Catℓ = Cat ℓ ℓ + open import Cat.Categories.Fun + open Functor + module _ (ℂ 𝔻 : Category ℓ ℓ) where + private + :obj: : Cat ℓ ℓ .Object + :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻} - -- 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₂) + :func*: : Functor ℂ 𝔻 × ℂ .Object → 𝔻 .Object + :func*: (F , A) = F .func* A - x : Functor X :product: - x = record - { func* = λ x → (func* x₁) x , (func* x₂) x - ; func→ = λ x → func→ x₁ x , func→ x₂ x - ; ident = lift-eq (ident x₁) (ident x₂) - ; distrib = lift-eq (distrib x₁) (distrib x₂) + 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 × ℂ .Arrow A B) + → 𝔻 .Arrow (F .func* A) (G .func* B) + :func→: ((θ , θNat) , f) = result + where + _𝔻⊕_ = 𝔻 ._⊕_ + θA : 𝔻 .Arrow (F .func* A) (G .func* A) + θA = θ A + θB : 𝔻 .Arrow (F .func* B) (G .func* B) + θB = θ B + F→f : 𝔻 .Arrow (F .func* A) (F .func* B) + F→f = F .func→ f + G→f : 𝔻 .Arrow (G .func* A) (G .func* B) + G→f = G .func→ f + l : 𝔻 .Arrow (F .func* A) (G .func* B) + l = θB 𝔻⊕ F→f + r : 𝔻 .Arrow (F .func* A) (G .func* 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 : 𝔻 .Arrow (F .func* A) (G .func* B) + result = l + + _×p_ = product + + 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₂ 𝔻.ident) (F .ident) + where + _𝔻⊕_ = 𝔻 ._⊕_ + open module 𝔻 = IsCategory (𝔻 .isCategory) + -- Unfortunately the equational version has some ambigous arguments. + -- :ident: : :func→: (identityNat F , ℂ .𝟙 {o = proj₂ c}) ≡ 𝔻 .𝟙 + -- :ident: = begin + -- :func→: ((:obj: ×p ℂ) .Product.obj .𝟙) ≡⟨⟩ + -- :func→: (identityNat F , ℂ .𝟙) ≡⟨⟩ + -- (identityTrans F C 𝔻⊕ F .func→ (ℂ .𝟙)) ≡⟨⟩ + -- (𝔻 .𝟙 𝔻⊕ F .func→ (ℂ .𝟙)) ≡⟨ proj₂ 𝔻.ident ⟩ + -- F .func→ (ℂ .𝟙) ≡⟨ F .ident ⟩ + -- 𝔻 .𝟙 ∎ + -- where + -- _𝔻⊕_ = 𝔻 ._⊕_ + -- open module 𝔻 = IsCategory (𝔻 .isCategory) + 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⊕_ = (:obj: ×p ℂ) .Product.obj ._⊕_ {F×A} {G×B} {H×C} + module _ + -- NaturalTransformation F G × ℂ .Arrow A B + {θ×α : NaturalTransformation F G × ℂ .Arrow A B} + {η×β : NaturalTransformation G H × ℂ .Arrow B C} where + θ : Transformation F G + θ = proj₁ (proj₁ θ×α) + θNat : Natural F G θ + θNat = proj₂ (proj₁ θ×α) + f : ℂ .Arrow A B + f = proj₂ θ×α + η : Transformation G H + η = proj₁ (proj₁ η×β) + ηNat : Natural G H η + ηNat = proj₂ (proj₁ η×β) + g : ℂ .Arrow B C + g = proj₂ η×β + -- :func→: ((θ , θNat) , f) = θB 𝔻⊕ F→f + _ : (:func→: {F×A} {G×B} θ×α) ≡ (θ B 𝔻⊕ F .func→ f) + _ = refl + ηθ : NaturalTransformation F H + ηθ = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat) + _ : ηθ ≡ Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat) + _ = refl + ηθT = proj₁ ηθ + ηθN = proj₂ ηθ + _ : ηθT ≡ λ T → η T 𝔻⊕ θ T -- Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat) + _ = refl + :distrib: : + :func→: {F×A} {H×C} (η×β P⊕ θ×α) + ≡ (:func→: {G×B} {H×C} η×β) 𝔻⊕ (:func→: {F×A} {G×B} θ×α) + :distrib: = begin + :func→: {F×A} {H×C} (η×β P⊕ θ×α) ≡⟨⟩ + :func→: {F×A} {H×C} (ηθ , g ℂ⊕ f) ≡⟨⟩ + (ηθT C 𝔻⊕ F .func→ (g ℂ⊕ f)) ≡⟨ ηθN (g ℂ⊕ f) ⟩ + (H .func→ (g ℂ⊕ f) 𝔻⊕ ηθT A) ≡⟨ cong (λ φ → φ 𝔻⊕ ηθT A) (H .distrib) ⟩ + ((H .func→ g 𝔻⊕ H .func→ f) 𝔻⊕ ηθT A) ≡⟨ sym 𝔻.assoc ⟩ + (H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ ηθT A)) ≡⟨⟩ + (H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (η A 𝔻⊕ θ A))) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) 𝔻.assoc ⟩ + (H .func→ g 𝔻⊕ ((H .func→ f 𝔻⊕ η A) 𝔻⊕ θ A)) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (cong (λ φ → φ 𝔻⊕ θ A) (sym (ηNat f))) ⟩ + (H .func→ g 𝔻⊕ ((η B 𝔻⊕ G .func→ f) 𝔻⊕ θ A)) ≡⟨ cong (λ φ → H .func→ g 𝔻⊕ φ) (sym 𝔻.assoc) ⟩ + (H .func→ g 𝔻⊕ (η B 𝔻⊕ (G .func→ f 𝔻⊕ θ A))) ≡⟨ 𝔻.assoc ⟩ + ((H .func→ g 𝔻⊕ η B) 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ cong (λ φ → φ 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) (sym (ηNat g)) ⟩ + ((η C 𝔻⊕ G .func→ g) 𝔻⊕ (G .func→ f 𝔻⊕ θ A)) ≡⟨ cong (λ φ → (η C 𝔻⊕ G .func→ g) 𝔻⊕ φ) (sym (θNat f)) ⟩ + ((η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f)) ≡⟨⟩ + ((:func→: {G×B} {H×C} η×β) 𝔻⊕ (:func→: {F×A} {G×B} θ×α)) ∎ + where + lemθ : θ B 𝔻⊕ F .func→ f ≡ G .func→ f 𝔻⊕ θ A + lemθ = θNat f + lemη : η C 𝔻⊕ G .func→ g ≡ H .func→ g 𝔻⊕ η B + lemη = ηNat g + lemm : ηθT C 𝔻⊕ F .func→ (g ℂ⊕ f) ≡ (H .func→ (g ℂ⊕ f) 𝔻⊕ ηθT A) + lemm = ηθN (g ℂ⊕ f) + final : η B 𝔻⊕ G .func→ f ≡ H .func→ f 𝔻⊕ η A + final = ηNat f + open module 𝔻 = IsCategory (𝔻 .isCategory) + -- Type of `:eval:` is aka.: + -- Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 + -- :eval: : Cat ℓ ℓ .Arrow ((:obj: ×p ℂ) .Product.obj) 𝔻 + :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 + :eval: = record + { func* = :func*: + ; func→ = λ {dom} {cod} → :func→: {dom} {cod} + ; ident = λ {o} → :ident: {o} + ; distrib = λ {f u n k y} → :distrib: {f} {u} {n} {k} {y} } - -- Need to "lift equality of functors" - -- If I want to do this like I do it for pairs it's gonna be a pain. - postulate isUniqL : (Cat ⊕ proj₁) x ≡ x₁ - -- isUniqL = lift-eq-functors refl refl {!!} {!!} + module _ (𝔸 : Category ℓ ℓ) (F : Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻) where + instance + CatℓHasProducts : HasProducts Catℓ + CatℓHasProducts = CatHasProducts {ℓ} {ℓ} + t : Catℓ .Arrow ((𝔸 ×p ℂ) .Product.obj) 𝔻 ≡ Functor ((𝔸 ×p ℂ) .Product.obj) 𝔻 + t = refl + tt : Category ℓ ℓ + tt = (𝔸 ×p ℂ) .Product.obj + open HasProducts CatℓHasProducts + postulate + transpose : Functor 𝔸 :obj: + eq : Catℓ ._⊕_ :eval: (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ≡ F - postulate isUniqR : (Cat ⊕ proj₂) x ≡ x₂ - -- isUniqR = lift-eq-functors refl refl {!!} {!!} + catTranspose : ∃![ F~ ] (Catℓ ._⊕_ :eval: (parallelProduct F~ (Catℓ .𝟙 {o = ℂ})) ≡ F) + catTranspose = transpose , eq - isUniq : (Cat ⊕ proj₁) x ≡ x₁ × (Cat ⊕ proj₂) x ≡ x₂ - isUniq = isUniqL , isUniqR + -- :isExponential: : IsExponential Catℓ A B :obj: {!:eval:!} + :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: + :isExponential: = catTranspose - uniq : ∃![ x ] ((Cat ⊕ proj₁) x ≡ x₁ × (Cat ⊕ proj₂) x ≡ x₂) - uniq = x , isUniq + -- :exponent: : Exponential (Cat ℓ ℓ) A B + :exponent: : Exponential Catℓ ℂ 𝔻 + :exponent: = record + { obj = :obj: + ; eval = :eval: + ; isExponential = :isExponential: + } - instance - isProduct : IsProduct Cat proj₁ proj₂ - isProduct = uniq - - product : Product {ℂ = Cat} C D - product = record - { obj = :product: - ; proj₁ = proj₁ - ; proj₂ = proj₂ - } + CatHasExponentials : HasExponentials Catℓ + CatHasExponentials = record { exponent = :exponent: } diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 3d01ffa..c818e76 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -13,7 +13,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat open Category open Functor - module _ (F : Functor ℂ 𝔻) (G : Functor ℂ 𝔻) where + module _ (F G : Functor ℂ 𝔻) where -- What do you call a non-natural tranformation? Transformation : Set (ℓc ⊔ ℓd') Transformation = (C : ℂ .Object) → 𝔻 .Arrow (F .func* C) (G .func* C) diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index 3579b52..cec4043 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -11,16 +11,35 @@ open import Cat.Category open import Cat.Functor open Category -Sets : {ℓ : Level} → Category (lsuc ℓ) ℓ -Sets {ℓ} = record - { Object = Set ℓ - ; Arrow = λ T U → T → U - ; 𝟙 = id - ; _⊕_ = _∘′_ - ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) } - } - where - open import Function +module _ {ℓ : Level} where + Sets : Category (lsuc ℓ) ℓ + Sets = record + { Object = Set ℓ + ; Arrow = λ T U → T → U + ; 𝟙 = id + ; _⊕_ = _∘′_ + ; isCategory = record { assoc = refl ; ident = funExt (λ _ → refl) , funExt (λ _ → refl) } + } + where + open import Function + + private + module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where + pair : (X → A × B) + pair x = f x , g x + lem : Sets ._⊕_ proj₁ pair ≡ f × Sets ._⊕_ snd pair ≡ g + proj₁ lem = refl + snd lem = refl + instance + isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} fst snd + isProduct f g = pair f g , lem f g + + product : (A B : Sets .Object) → Product {ℂ = Sets} A B + product A B = record { obj = A × B ; proj₁ = fst ; proj₂ = snd ; isProduct = {!!} } + + instance + SetsHasProducts : HasProducts Sets + SetsHasProducts = record { product = product } -- Covariant Presheaf Representable : {ℓ ℓ' : Level} → (ℂ : Category ℓ ℓ') → Set (ℓ ⊔ lsuc ℓ') diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 1c8c12f..1d826da 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -88,6 +88,7 @@ record Product {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} (A B : ℂ .Object) proj₁ : ℂ .Arrow obj A proj₂ : ℂ .Arrow obj B {{isProduct}} : IsProduct ℂ proj₁ proj₂ + arrowProduct : ∀ {X} → (π₁ : Arrow ℂ X A) (π₂ : Arrow ℂ X B) → Arrow ℂ X obj arrowProduct π₁ π₂ = fst (isProduct π₁ π₂) @@ -96,6 +97,18 @@ record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ field product : ∀ (A B : ℂ .Object) → Product {ℂ = ℂ} A B + open Product + + objectProduct : (A B : ℂ .Object) → ℂ .Object + objectProduct 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 + parallelProduct : {A A' B B' : ℂ .Object} → ℂ .Arrow A A' → ℂ .Arrow B B' + → ℂ .Arrow (objectProduct A B) (objectProduct A' B') + parallelProduct {A = A} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B') + (ℂ ._⊕_ a ((product A B) .proj₁)) + (ℂ ._⊕_ b ((product A B) .proj₂)) + module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where Opposite : Category ℓ ℓ' Opposite = @@ -127,3 +140,37 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where HomFromArrow : (A : ℂ .Object) → {B B' : ℂ .Object} → (g : ℂ .Arrow B B') → Hom ℂ A B → Hom ℂ A B' HomFromArrow _A = _⊕_ ℂ + +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) + + module _ (B C : ℂ .Category.Object) where + IsExponential : (Cᴮ : ℂ .Object) → ℂ .Arrow (Cᴮ ×p B) C → Set (ℓ ⊔ ℓ') + IsExponential Cᴮ eval = ∀ (A : ℂ .Object) (f : ℂ .Arrow (A ×p B) C) + → ∃![ f~ ] (ℂ ._⊕_ eval (parallelProduct f~ (ℂ .𝟙)) ≡ f) + + record Exponential : Set (ℓ ⊔ ℓ') where + field + -- obj ≡ Cᴮ + obj : ℂ .Object + eval : ℂ .Arrow ( obj ×p B ) C + {{isExponential}} : IsExponential obj eval + -- If I make this an instance-argument then the instance resolution + -- algorithm goes into an infinite loop. Why? + productsFromExp : HasProducts ℂ + productsFromExp = ℂHasProducts + transpose : (A : ℂ .Object) → ℂ .Arrow (A ×p B) C → ℂ .Arrow A obj + transpose A f = fst (isExponential A f) + +record HasExponentials {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') {{_ : HasProducts ℂ}} : Set (ℓ ⊔ ℓ') where + field + exponent : (A B : ℂ .Object) → Exponential ℂ A B + +record CartesianClosed {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where + field + {{hasProducts}} : HasProducts ℂ + {{hasExponentials}} : HasExponentials ℂ diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 9d3293e..78baf35 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --allow-unsolved-metas --cubical #-} module Cat.Category.Properties where @@ -48,33 +48,25 @@ epi-mono-is-not-iso f = in {!!} -} + open import Cat.Categories.Cat + open Exponential + open HasExponentials CatHasExponentials -module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} (B C : ℂ .Category.Object) where - open Category - open HasProducts hasProducts - open Product - prod-obj : (A B : ℂ .Object) → ℂ .Object - prod-obj 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 A' B B' : ℂ .Object} → ℂ .Arrow A A' → ℂ .Arrow B B' - → ℂ .Arrow (prod-obj A B) (prod-obj A' B') - ×A {A = A} {A' = A'} {B = B} {B' = B'} a b = arrowProduct (product A' B') - (ℂ ._⊕_ a ((product A B) .proj₁)) - (ℂ ._⊕_ b ((product A B) .proj₂)) + Exp : Set {!!} + Exp = Exponential (Cat {!!} {!!}) {{ℂHasProducts = {!!}}} + Sets (Opposite {!!}) - IsExponential : {Cᴮ : ℂ .Object} → ℂ .Arrow (prod-obj Cᴮ B) C → Set (ℓ ⊔ ℓ') - IsExponential eval = ∀ (A : ℂ .Object) (f : ℂ .Arrow (prod-obj A B) C) - → ∃![ f~ ] (ℂ ._⊕_ eval (×A f~ (ℂ .𝟙)) ≡ f) + -- _⇑_ : (A B : Catℓ .Object) → Catℓ .Object + -- A ⇑ B = (exponent A B) .obj - record Exponential : Set (ℓ ⊔ ℓ') where - field - -- obj ≡ Cᴮ - obj : ℂ .Object - eval : ℂ .Arrow ( prod-obj obj B ) C - {{isExponential}} : IsExponential eval + -- private + -- :func*: : ℂ .Object → (Sets ⇑ Opposite ℂ) .Object + -- :func*: x = {!!} -_⇑_ = Exponential - --- yoneda : ∀ {ℓ ℓ'} → {ℂ : Category ℓ ℓ'} → Functor ℂ (Sets ⇑ (Opposite ℂ)) --- yoneda = {!!} + -- yoneda : Functor ℂ (Sets ⇑ (Opposite ℂ)) + -- yoneda = record + -- { func* = :func*: + -- ; func→ = {!!} + -- ; ident = {!!} + -- ; distrib = {!!} + -- }