From 3fcdf828d849a6c36cb7bb40e38d125a73226231 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Sun, 21 Jan 2018 21:29:15 +0100 Subject: [PATCH 01/10] Implement exponentials --- src/Cat/Category.agda | 7 ++++++ src/Cat/Category/Properties.agda | 37 ++++++++++++++++++++++---------- 2 files changed, 33 insertions(+), 11 deletions(-) diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 91e25f3..1c8c12f 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -88,6 +88,13 @@ 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 π₁ π₂) + +record HasProducts {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') : Set (ℓ ⊔ ℓ') where + field + product : ∀ (A B : ℂ .Object) → Product {ℂ = ℂ} A B module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where Opposite : Category ℓ ℓ' diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 4ff4376..9d3293e 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -49,17 +49,32 @@ epi-mono-is-not-iso f = -} -module _ {ℓa ℓa' ℓb ℓb'} where - Exponential : Category ℓa ℓa' → Category ℓb ℓb' → Category {!!} {!!} - Exponential A B = record - { Object = {!!} - ; Arrow = {!!} - ; 𝟙 = {!!} - ; _⊕_ = {!!} - ; isCategory = {!!} - } +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₂)) + + 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) + + record Exponential : Set (ℓ ⊔ ℓ') where + field + -- obj ≡ Cᴮ + obj : ℂ .Object + eval : ℂ .Arrow ( prod-obj obj B ) C + {{isExponential}} : IsExponential eval _⇑_ = Exponential -yoneda : ∀ {ℓ ℓ'} → {ℂ : Category ℓ ℓ'} → Functor ℂ (Sets ⇑ (Opposite ℂ)) -yoneda = {!!} +-- yoneda : ∀ {ℓ ℓ'} → {ℂ : Category ℓ ℓ'} → Functor ℂ (Sets ⇑ (Opposite ℂ)) +-- yoneda = {!!} From bf1d1566af70051fe003b9c08581b0a380141642 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 22 Jan 2018 00:04:19 +0100 Subject: [PATCH 02/10] Naturality; category of functors and natural transformations WIP --- src/Cat.agda | 1 + src/Cat/Naturality.agda | 102 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 103 insertions(+) create mode 100644 src/Cat/Naturality.agda diff --git a/src/Cat.agda b/src/Cat.agda index 6cb8e32..1319eb6 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -10,3 +10,4 @@ import Cat.Category.Properties import Cat.Category import Cat.Cubical import Cat.Functor +import Cat.Naturality diff --git a/src/Cat/Naturality.agda b/src/Cat/Naturality.agda new file mode 100644 index 0000000..c6ba91f --- /dev/null +++ b/src/Cat/Naturality.agda @@ -0,0 +1,102 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module Cat.Naturality where + +open import Agda.Primitive +open import Cubical +open import Function +open import Data.Product + +open import Cat.Category +open import Cat.Functor + +module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Category ℓd ℓd'} where + open Category + open Functor + + module _ (F : Functor ℂ 𝔻) (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) + + Natural : Transformation → Set (ℓc ⊔ (ℓc' ⊔ ℓd')) + Natural θ + = {A B : ℂ .Object} + → (f : ℂ .Arrow A B) + → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A) + + NaturalTranformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') + NaturalTranformation = Σ Transformation Natural + + -- NaturalTranformation : Set (ℓc ⊔ (ℓc' ⊔ ℓd')) + -- NaturalTranformation = ∀ (θ : Transformation) {A B : ℂ .Object} → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A) + + 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₂ 𝔻.ident ⟩ + F→ f ≡⟨ sym (proj₁ 𝔻.ident) ⟩ + F→ f 𝔻⊕ 𝔻 .𝟙 ≡⟨⟩ + F→ f 𝔻⊕ identityTrans F A ∎ + where + _𝔻⊕_ = 𝔻 ._⊕_ + F→ = F .func→ + open module 𝔻 = IsCategory (𝔻 .isCategory) + + identityNat : (F : Functor ℂ 𝔻) → NaturalTranformation F F + identityNat F = identityTrans F , identityNatural F + + module _ {a b c : Functor ℂ 𝔻} where + private + _𝔻⊕_ = 𝔻 ._⊕_ + _∘nt_ : Transformation b c → Transformation a b → Transformation a c + (θ ∘nt η) C = θ C 𝔻⊕ η C + + _:⊕:_ : NaturalTranformation b c → NaturalTranformation a b → NaturalTranformation a c + proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η + proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin + ((θ ∘nt η) B) 𝔻⊕ (a .func→ f) ≡⟨⟩ + (θ B 𝔻⊕ η B) 𝔻⊕ (a .func→ f) ≡⟨ sym assoc ⟩ + θ B 𝔻⊕ (η B 𝔻⊕ (a .func→ f)) ≡⟨ cong (λ φ → θ B 𝔻⊕ φ) (ηNat f) ⟩ + θ B 𝔻⊕ ((b .func→ f) 𝔻⊕ η A) ≡⟨ assoc ⟩ + (θ B 𝔻⊕ (b .func→ f)) 𝔻⊕ η A ≡⟨ cong (λ φ → φ 𝔻⊕ η A) (θNat f) ⟩ + (((c .func→ f) 𝔻⊕ θ A) 𝔻⊕ η A) ≡⟨ sym assoc ⟩ + ((c .func→ f) 𝔻⊕ (θ A 𝔻⊕ η A)) ≡⟨⟩ + ((c .func→ f) 𝔻⊕ ((θ ∘nt η) A)) ∎ + where + open IsCategory (𝔻 .isCategory) + + private + module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTranformation A B} + {g : NaturalTranformation B C} {h : NaturalTranformation C D} where + _g⊕f_ = _:⊕:_ {A} {B} {C} + _h⊕g_ = _:⊕:_ {B} {C} {D} + :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f) + :assoc: = {!!} + module _ {A B : Functor ℂ 𝔻} {f : NaturalTranformation A B} where + ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f + ident-r = {!!} + ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f + ident-l = {!!} + :ident: + : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f + × (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f + :ident: = ident-r , ident-l + + instance + :isCategory: : IsCategory (Functor ℂ 𝔻) NaturalTranformation + (λ {F} → identityNat F) (λ {a} {b} {c} → _:⊕:_ {a} {b} {c}) + :isCategory: = record + { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D} + ; ident = λ {A B} → :ident: {A} {B} + } + + aCat : Category (ℓc ⊔ (ℓc' ⊔ (ℓd ⊔ ℓd'))) (ℓc ⊔ (ℓc' ⊔ ℓd')) + aCat = record + { Object = Functor ℂ 𝔻 + ; Arrow = NaturalTranformation + ; 𝟙 = λ {F} → identityNat F + ; _⊕_ = λ {a b c} → _:⊕:_ {a} {b} {c} + } From 9fdf6b589bc32a38c3abcb05e47b81e0284e0831 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 22 Jan 2018 11:35:37 +0100 Subject: [PATCH 03/10] Use TDNR in Functor --- proposal/macros.tex | 1 + src/Cat/Functor.agda | 14 ++++++-------- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/proposal/macros.tex b/proposal/macros.tex index 604ae8b..aec0c67 100644 --- a/proposal/macros.tex +++ b/proposal/macros.tex @@ -5,6 +5,7 @@ \newcommand{\defeq}{\coloneqq} \newcommand{\bN}{\mathbb{N}} \newcommand{\bC}{\mathbb{C}} +\newcommand{\bX}{\mathbb{X}} \newcommand{\to}{\rightarrow}} \newcommand{\mto}{\mapsto}} \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace} diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda index 5965f72..c0bebc1 100644 --- a/src/Cat/Functor.agda +++ b/src/Cat/Functor.agda @@ -8,18 +8,16 @@ open import Cat.Category record Functor {ℓc ℓc' ℓd ℓd'} (C : Category ℓc ℓc') (D : Category ℓd ℓd') : Set (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') where - private - open module C = Category C - open module D = Category D + open Category field - func* : C.Object → D.Object - func→ : {dom cod : C.Object} → C.Arrow dom cod → D.Arrow (func* dom) (func* cod) - ident : { c : C.Object } → func→ (C.𝟙 {c}) ≡ D.𝟙 {func* c} + func* : C .Object → D .Object + func→ : {dom cod : C .Object} → C .Arrow dom cod → D .Arrow (func* dom) (func* cod) + ident : { c : C .Object } → func→ (C .𝟙 {c}) ≡ D .𝟙 {func* c} -- TODO: Avoid use of ugly explicit arguments somehow. -- This guy managed to do it: -- https://github.com/copumpkin/categories/blob/master/Categories/Functor/Core.agda - distrib : { c c' c'' : C.Object} {a : C.Arrow c c'} {a' : C.Arrow c' c''} - → func→ (a' C.⊕ a) ≡ func→ a' D.⊕ func→ a + distrib : { c c' c'' : C .Object} {a : C .Arrow c c'} {a' : C .Arrow c' c''} + → func→ (C ._⊕_ a' a) ≡ D ._⊕_ (func→ a') (func→ a) module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where open Functor From fd03049c92778996578a8ea4590ded09205df813 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 22 Jan 2018 14:44:25 +0100 Subject: [PATCH 04/10] Move the category of functors --- src/Cat.agda | 14 +++++++------- src/Cat/{Naturality.agda => Categories/Fun.agda} | 7 ++++--- 2 files changed, 11 insertions(+), 10 deletions(-) rename src/Cat/{Naturality.agda => Categories/Fun.agda} (95%) diff --git a/src/Cat.agda b/src/Cat.agda index 1319eb6..cf6a174 100644 --- a/src/Cat.agda +++ b/src/Cat.agda @@ -1,13 +1,13 @@ module Cat where -import Cat.Categories.Sets -import Cat.Categories.Cat -import Cat.Categories.Rel +import Cat.Cubical +import Cat.Category +import Cat.Functor import Cat.Category.Pathy import Cat.Category.Bij import Cat.Category.Free import Cat.Category.Properties -import Cat.Category -import Cat.Cubical -import Cat.Functor -import Cat.Naturality +import Cat.Categories.Sets +import Cat.Categories.Cat +import Cat.Categories.Rel +import Cat.Categories.Fun diff --git a/src/Cat/Naturality.agda b/src/Cat/Categories/Fun.agda similarity index 95% rename from src/Cat/Naturality.agda rename to src/Cat/Categories/Fun.agda index c6ba91f..4be2d3d 100644 --- a/src/Cat/Naturality.agda +++ b/src/Cat/Categories/Fun.agda @@ -1,5 +1,5 @@ {-# OPTIONS --allow-unsolved-metas #-} -module Cat.Naturality where +module Cat.Categories.Fun where open import Agda.Primitive open import Cubical @@ -93,8 +93,9 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat ; ident = λ {A B} → :ident: {A} {B} } - aCat : Category (ℓc ⊔ (ℓc' ⊔ (ℓd ⊔ ℓd'))) (ℓc ⊔ (ℓc' ⊔ ℓd')) - aCat = record + -- Functor categories. Objects are functors, arrows are natural transformations. + Fun : Category (ℓc ⊔ (ℓc' ⊔ (ℓd ⊔ ℓd'))) (ℓc ⊔ (ℓc' ⊔ ℓd')) + Fun = record { Object = Functor ℂ 𝔻 ; Arrow = NaturalTranformation ; 𝟙 = λ {F} → identityNat F From dd3415a69dd442c88e448f0e6c7525d8c04c53db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 22 Jan 2018 14:44:50 +0100 Subject: [PATCH 05/10] Some stuff about CwF's --- src/Cat/Cubical.agda | 50 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 49 insertions(+), 1 deletion(-) diff --git a/src/Cat/Cubical.agda b/src/Cat/Cubical.agda index b10afba..bc3baae 100644 --- a/src/Cat/Cubical.agda +++ b/src/Cat/Cubical.agda @@ -7,14 +7,62 @@ open import Data.Product open import Data.Sum open import Data.Unit open import Data.Empty +open import Data.Product open import Cat.Category +open import Cat.Functor -- See chapter 1 for a discussion on how presheaf categories are CwF's. -- See section 6.8 in Huber's thesis for details on how to implement the -- categorical version of CTT +module CwF {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where + open Category + open Functor + open import Function + open import Cubical + + module _ {ℓa ℓb : Level} where + private + Obj = Σ[ A ∈ Set ℓa ] (A → Set ℓb) + Arr : Obj → Obj → Set (ℓa ⊔ ℓb) + Arr (A , B) (A' , B') = Σ[ f ∈ (A → A') ] ({x : A} → B x → B' (f x)) + one : {o : Obj} → Arr o o + proj₁ one = λ x → x + proj₂ one = λ b → b + _:⊕:_ : {a b c : Obj} → Arr b c → Arr a b → Arr a c + (g , g') :⊕: (f , f') = g ∘ f , g' ∘ f' + + module _ {A B C D : Obj} {f : Arr A B} {g : Arr B C} {h : Arr C D} where + :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f) + :assoc: = {!!} + + module _ {A B : Obj} {f : Arr A B} where + :ident: : (_:⊕:_ {A} {A} {B} f one) ≡ f × (_:⊕:_ {A} {B} {B} one f) ≡ f + :ident: = {!!} + + instance + :isCategory: : IsCategory Obj Arr one (λ {a b c} → _:⊕:_ {a} {b} {c}) + :isCategory: = record + { assoc = λ {A} {B} {C} {D} {f} {g} {h} → :assoc: {A} {B} {C} {D} {f} {g} {h} + ; ident = {!!} + } + Fam : Category (lsuc (ℓa ⊔ ℓb)) (ℓa ⊔ ℓb) + Fam = record + { Object = Obj + ; Arrow = Arr + ; 𝟙 = one + ; _⊕_ = λ {a b c} → _:⊕:_ {a} {b} {c} + } + + Contexts = ℂ .Object + Substitutions = ℂ .Arrow + + record CwF : Set {!ℓa ⊔ ℓb!} where + field + Terms : Functor (Opposite ℂ) Fam + module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where -- Ns is the "namespace" ℓo = (lsuc lzero ⊔ ℓ) @@ -49,5 +97,5 @@ module _ {ℓ ℓ' : Level} (Ns : Set ℓ) where ; Arrow = Mor ; 𝟙 = {!!} ; _⊕_ = {!!} - ; isCategory = ? + ; isCategory = {!!} } From 6a25a4c3ff519ec1b6da7917cc61297227ceffed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Mon, 22 Jan 2018 15:03:04 +0100 Subject: [PATCH 06/10] Fix typo, rename implicit variables, implement presheaf --- src/Cat/Categories/Fun.agda | 55 +++++++++++++++++++++++-------------- 1 file changed, 34 insertions(+), 21 deletions(-) diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda index 4be2d3d..3d01ffa 100644 --- a/src/Cat/Categories/Fun.agda +++ b/src/Cat/Categories/Fun.agda @@ -24,8 +24,8 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat → (f : ℂ .Arrow A B) → 𝔻 ._⊕_ (θ B) (F .func→ f) ≡ 𝔻 ._⊕_ (G .func→ f) (θ A) - NaturalTranformation : Set (ℓc ⊔ ℓc' ⊔ ℓd') - NaturalTranformation = Σ Transformation Natural + 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) @@ -45,37 +45,38 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat F→ = F .func→ open module 𝔻 = IsCategory (𝔻 .isCategory) - identityNat : (F : Functor ℂ 𝔻) → NaturalTranformation F F + identityNat : (F : Functor ℂ 𝔻) → NaturalTransformation F F identityNat F = identityTrans F , identityNatural F - module _ {a b c : Functor ℂ 𝔻} where + module _ {F G H : Functor ℂ 𝔻} where private _𝔻⊕_ = 𝔻 ._⊕_ - _∘nt_ : Transformation b c → Transformation a b → Transformation a c + _∘nt_ : Transformation G H → Transformation F G → Transformation F H (θ ∘nt η) C = θ C 𝔻⊕ η C - _:⊕:_ : NaturalTranformation b c → NaturalTranformation a b → NaturalTranformation a c + NatComp _:⊕:_ : NaturalTransformation G H → NaturalTransformation F G → NaturalTransformation F H proj₁ ((θ , _) :⊕: (η , _)) = θ ∘nt η proj₂ ((θ , θNat) :⊕: (η , ηNat)) {A} {B} f = begin - ((θ ∘nt η) B) 𝔻⊕ (a .func→ f) ≡⟨⟩ - (θ B 𝔻⊕ η B) 𝔻⊕ (a .func→ f) ≡⟨ sym assoc ⟩ - θ B 𝔻⊕ (η B 𝔻⊕ (a .func→ f)) ≡⟨ cong (λ φ → θ B 𝔻⊕ φ) (ηNat f) ⟩ - θ B 𝔻⊕ ((b .func→ f) 𝔻⊕ η A) ≡⟨ assoc ⟩ - (θ B 𝔻⊕ (b .func→ f)) 𝔻⊕ η A ≡⟨ cong (λ φ → φ 𝔻⊕ η A) (θNat f) ⟩ - (((c .func→ f) 𝔻⊕ θ A) 𝔻⊕ η A) ≡⟨ sym assoc ⟩ - ((c .func→ f) 𝔻⊕ (θ A 𝔻⊕ η A)) ≡⟨⟩ - ((c .func→ f) 𝔻⊕ ((θ ∘nt η) A)) ∎ + ((θ ∘nt η) B) 𝔻⊕ (F .func→ f) ≡⟨⟩ + (θ B 𝔻⊕ η B) 𝔻⊕ (F .func→ f) ≡⟨ sym assoc ⟩ + θ B 𝔻⊕ (η B 𝔻⊕ (F .func→ f)) ≡⟨ cong (λ φ → θ B 𝔻⊕ φ) (ηNat f) ⟩ + θ B 𝔻⊕ ((G .func→ f) 𝔻⊕ η A) ≡⟨ assoc ⟩ + (θ B 𝔻⊕ (G .func→ f)) 𝔻⊕ η A ≡⟨ cong (λ φ → φ 𝔻⊕ η A) (θNat f) ⟩ + (((H .func→ f) 𝔻⊕ θ A) 𝔻⊕ η A) ≡⟨ sym assoc ⟩ + ((H .func→ f) 𝔻⊕ (θ A 𝔻⊕ η A)) ≡⟨⟩ + ((H .func→ f) 𝔻⊕ ((θ ∘nt η) A)) ∎ where open IsCategory (𝔻 .isCategory) + NatComp = _:⊕:_ private - module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTranformation A B} - {g : NaturalTranformation B C} {h : NaturalTranformation C D} where + module _ {A B C D : Functor ℂ 𝔻} {f : NaturalTransformation A B} + {g : NaturalTransformation B C} {h : NaturalTransformation C D} where _g⊕f_ = _:⊕:_ {A} {B} {C} _h⊕g_ = _:⊕:_ {B} {C} {D} :assoc: : (_:⊕:_ {A} {C} {D} h (_:⊕:_ {A} {B} {C} g f)) ≡ (_:⊕:_ {A} {B} {D} (_:⊕:_ {B} {C} {D} h g) f) :assoc: = {!!} - module _ {A B : Functor ℂ 𝔻} {f : NaturalTranformation A B} where + module _ {A B : Functor ℂ 𝔻} {f : NaturalTransformation A B} where ident-r : (_:⊕:_ {A} {A} {B} f (identityNat A)) ≡ f ident-r = {!!} ident-l : (_:⊕:_ {A} {B} {B} (identityNat B) f) ≡ f @@ -86,7 +87,7 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat :ident: = ident-r , ident-l instance - :isCategory: : IsCategory (Functor ℂ 𝔻) NaturalTranformation + :isCategory: : IsCategory (Functor ℂ 𝔻) NaturalTransformation (λ {F} → identityNat F) (λ {a} {b} {c} → _:⊕:_ {a} {b} {c}) :isCategory: = record { assoc = λ {A B C D} → :assoc: {A} {B} {C} {D} @@ -94,10 +95,22 @@ module _ {ℓc ℓc' ℓd ℓd' : Level} {ℂ : Category ℓc ℓc'} {𝔻 : Cat } -- Functor categories. Objects are functors, arrows are natural transformations. - Fun : Category (ℓc ⊔ (ℓc' ⊔ (ℓd ⊔ ℓd'))) (ℓc ⊔ (ℓc' ⊔ ℓd')) + Fun : Category (ℓc ⊔ ℓc' ⊔ ℓd ⊔ ℓd') (ℓc ⊔ ℓc' ⊔ ℓd') Fun = record { Object = Functor ℂ 𝔻 - ; Arrow = NaturalTranformation + ; Arrow = NaturalTransformation ; 𝟙 = λ {F} → identityNat F - ; _⊕_ = λ {a b c} → _:⊕:_ {a} {b} {c} + ; _⊕_ = λ {F G H} → _:⊕:_ {F} {G} {H} + } + +module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where + open import Cat.Categories.Sets + + -- Restrict the functors to Presheafs. + Presh : Category (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ') + Presh = record + { Object = Presheaf ℂ + ; Arrow = NaturalTransformation + ; 𝟙 = λ {F} → identityNat F + ; _⊕_ = λ {F G H} → NatComp {F = F} {G = G} {H = H} } 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 07/10] 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 = {!!} + -- } From a480fca9563276b28291a2004b2dbd748adbe37c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 25 Jan 2018 12:01:37 +0100 Subject: [PATCH 08/10] Clean up some stuff --- src/Cat/Categories/Cat.agda | 154 +++++++++++++------------------ src/Cat/Categories/Sets.agda | 16 ++-- src/Cat/Category.agda | 8 +- src/Cat/Category/Properties.agda | 46 +++++---- 4 files changed, 107 insertions(+), 117 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index 61769b3..fae77fb 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -22,6 +22,7 @@ eqpair eqa eqb i = eqa i , eqb i open Functor open Category + module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where lift-eq-functors : {f g : Functor A B} → (eq* : f .func* ≡ g .func*) @@ -179,21 +180,24 @@ module _ {ℓ ℓ' : Level} where module _ {ℓ ℓ' : Level} where open Category instance - CatHasProducts : HasProducts (Cat ℓ ℓ') - CatHasProducts = record { product = product } + hasProducts : HasProducts (Cat ℓ ℓ') + hasProducts = record { product = product } -- Basically proves that `Cat ℓ ℓ` is cartesian closed. -module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ)}} where - open Data.Product - open Category - +module _ (ℓ : Level) where private - Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ) - Catℓ = Cat ℓ ℓ + open Data.Product + open Category open import Cat.Categories.Fun open Functor + + Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ) + Catℓ = Cat ℓ ℓ module _ (ℂ 𝔻 : Category ℓ ℓ) where private + _𝔻⊕_ = 𝔻 ._⊕_ + _ℂ⊕_ = ℂ ._⊕_ + :obj: : Cat ℓ ℓ .Object :obj: = Fun {ℂ = ℂ} {𝔻 = 𝔻} @@ -216,7 +220,6 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ) → 𝔻 .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) @@ -247,23 +250,22 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ) 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 ⟩ - -- 𝔻 .𝟙 ∎ + -- :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→: {c} {c} (identityNat F , ℂ .𝟙 {o = proj₂ c}) ≡ 𝔻 .𝟙 + :ident: = begin + :func→: {c} {c} ((:obj: ×p ℂ) .Product.obj .𝟙 {c}) ≡⟨⟩ + :func→: {c} {c} (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₂ @@ -271,68 +273,50 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ) 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 + {θ×f : NaturalTransformation F G × ℂ .Arrow A B} + {η×g : NaturalTransformation G H × ℂ .Arrow B C} where + private + θ : Transformation F G + θ = proj₁ (proj₁ θ×f) + θNat : Natural F G θ + θNat = proj₂ (proj₁ θ×f) + f : ℂ .Arrow A B + f = proj₂ θ×f + η : Transformation G H + η = proj₁ (proj₁ η×g) + ηNat : Natural G H η + ηNat = proj₂ (proj₁ η×g) + g : ℂ .Arrow B C + g = proj₂ η×g + + ηθNT : NaturalTransformation F H + ηθNT = Fun ._⊕_ {F} {G} {H} (η , ηNat) (θ , θNat) + + ηθ = proj₁ ηθNT + ηθNat = proj₂ ηθNT + :distrib: : - :func→: {F×A} {H×C} (η×β P⊕ θ×α) - ≡ (:func→: {G×B} {H×C} η×β) 𝔻⊕ (:func→: {F×A} {G×B} θ×α) + (η C 𝔻⊕ θ C) 𝔻⊕ F .func→ (g ℂ⊕ f) + ≡ (η C 𝔻⊕ G .func→ g) 𝔻⊕ (θ B 𝔻⊕ F .func→ f) :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} θ×α)) ∎ + (ηθ C) 𝔻⊕ F .func→ (g ℂ⊕ f) ≡⟨ ηθNat (g ℂ⊕ f) ⟩ + H .func→ (g ℂ⊕ f) 𝔻⊕ (ηθ A) ≡⟨ cong (λ φ → φ 𝔻⊕ ηθ A) (H .distrib) ⟩ + (H .func→ g 𝔻⊕ H .func→ f) 𝔻⊕ (ηθ A) ≡⟨ sym assoc ⟩ + H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ A)) ≡⟨⟩ + H .func→ g 𝔻⊕ (H .func→ f 𝔻⊕ (ηθ 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) ∎ 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) 𝔻 + open IsCategory (𝔻 .isCategory) + :eval: : Functor ((:obj: ×p ℂ) .Product.obj) 𝔻 :eval: = record { func* = :func*: @@ -342,14 +326,8 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ) } 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 + open HasProducts (hasProducts {ℓ} {ℓ}) using (parallelProduct) + postulate transpose : Functor 𝔸 :obj: eq : Catℓ ._⊕_ :eval: (parallelProduct transpose (Catℓ .𝟙 {o = ℂ})) ≡ F @@ -369,5 +347,5 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} {{_ : HasProducts (Opposite ℂ) ; isExponential = :isExponential: } - CatHasExponentials : HasExponentials Catℓ - CatHasExponentials = record { exponent = :exponent: } + hasExponentials : HasExponentials (Cat ℓ ℓ) + hasExponentials = record { exponent = :exponent: } diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda index cec4043..98750cf 100644 --- a/src/Cat/Categories/Sets.agda +++ b/src/Cat/Categories/Sets.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --allow-unsolved-metas #-} - module Cat.Categories.Sets where open import Cubical.PathPrelude @@ -25,17 +23,19 @@ module _ {ℓ : Level} where 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 + _&&&_ : (X → A × B) + _&&&_ x = f x , g x + module _ {X A B : Set ℓ} (f : X → A) (g : X → B) where + _S⊕_ = Sets ._⊕_ + lem : proj₁ S⊕ (f &&& g) ≡ f × snd S⊕ (f &&& g) ≡ g proj₁ lem = refl - snd lem = refl + proj₂ lem = refl instance isProduct : {A B : Sets .Object} → IsProduct Sets {A} {B} fst snd - isProduct f g = pair f g , lem f g + isProduct f g = 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 = {!!} } + product A B = record { obj = A × B ; proj₁ = fst ; proj₂ = snd ; isProduct = isProduct } instance SetsHasProducts : HasProducts Sets diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda index 1d826da..9fd378a 100644 --- a/src/Cat/Category.agda +++ b/src/Cat/Category.agda @@ -141,8 +141,8 @@ module _ {ℓ ℓ' : Level} {ℂ : Category ℓ ℓ'} where → Hom ℂ A B → Hom ℂ A B' HomFromArrow _A = _⊕_ ℂ -module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{ℂHasProducts : HasProducts ℂ}} where - open HasProducts ℂHasProducts +module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{hasProducts : HasProducts ℂ}} where + open HasProducts hasProducts open Product hiding (obj) private _×p_ : (A B : ℂ .Object) → ℂ .Object @@ -161,8 +161,8 @@ module _ {ℓ ℓ'} (ℂ : Category ℓ ℓ') {{ℂHasProducts : HasProducts ℂ {{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 + exponentialsHaveProducts : HasProducts ℂ + exponentialsHaveProducts = hasProducts transpose : (A : ℂ .Object) → ℂ .Arrow (A ×p B) C → ℂ .Arrow A obj transpose A f = fst (isExponential A f) diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda index 78baf35..90bc1b8 100644 --- a/src/Cat/Category/Properties.agda +++ b/src/Cat/Category/Properties.agda @@ -48,25 +48,37 @@ epi-mono-is-not-iso f = in {!!} -} - open import Cat.Categories.Cat +module _ {ℓ : Level} {ℂ : Category ℓ ℓ} where + open import Cat.Category + open Category + open import Cat.Categories.Cat using (Cat) + module Cat = Cat.Categories.Cat open Exponential - open HasExponentials CatHasExponentials + private + Catℓ = Cat ℓ ℓ + CatHasExponentials : HasExponentials Catℓ + CatHasExponentials = Cat.hasExponentials ℓ - Exp : Set {!!} - Exp = Exponential (Cat {!!} {!!}) {{ℂHasProducts = {!!}}} - Sets (Opposite {!!}) + -- Exp : Set (lsuc (lsuc ℓ)) + -- Exp = Exponential (Cat (lsuc ℓ) ℓ) + -- Sets (Opposite ℂ) - -- _⇑_ : (A B : Catℓ .Object) → Catℓ .Object - -- A ⇑ B = (exponent A B) .obj + _⇑_ : (A B : Catℓ .Object) → Catℓ .Object + A ⇑ B = (exponent A B) .obj + where + open HasExponentials CatHasExponentials - -- private - -- :func*: : ℂ .Object → (Sets ⇑ Opposite ℂ) .Object - -- :func*: x = {!!} + private + -- I need `Sets` to be a `Category ℓ ℓ` but it simlpy isn't. + Setz : Category ℓ ℓ + Setz = {!Sets!} + :func*: : ℂ .Object → (Setz ⇑ Opposite ℂ) .Object + :func*: A = {!!} - -- yoneda : Functor ℂ (Sets ⇑ (Opposite ℂ)) - -- yoneda = record - -- { func* = :func*: - -- ; func→ = {!!} - -- ; ident = {!!} - -- ; distrib = {!!} - -- } + yoneda : Functor ℂ (Setz ⇑ (Opposite ℂ)) + yoneda = record + { func* = :func*: + ; func→ = {!!} + ; ident = {!!} + ; distrib = {!!} + } From 7a77ba230c7dbf6525634d1d2e890eaf5e8339bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 25 Jan 2018 12:11:50 +0100 Subject: [PATCH 09/10] Move functor-equality to functor module --- src/Cat/Categories/Cat.agda | 20 +------------------- src/Cat/Functor.agda | 24 ++++++++++++++++++++++-- 2 files changed, 23 insertions(+), 21 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index fae77fb..f303937 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -23,23 +23,6 @@ eqpair eqa eqb i = eqa i , eqb i open Functor open Category -module _ {ℓ ℓ' : Level} {A B : Category ℓ ℓ'} where - lift-eq-functors : {f g : Functor A B} - → (eq* : f .func* ≡ g .func*) - → (eq→ : PathP (λ i → ∀ {x y} → A .Arrow x y → B .Arrow (eq* i x) (eq* i y)) - (f .func→) (g .func→)) - -- → (eq→ : Functor.func→ f ≡ {!!}) -- Functor.func→ g) - -- Use PathP - -- directly to show heterogeneous equalities by using previous - -- equalities (i.e. continuous paths) to create new continuous paths. - → (eqI : PathP (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ B .𝟙 {eq* i c}) - (ident f) (ident g)) - → (eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''} - → eq→ i (A ._⊕_ a' a) ≡ B ._⊕_ (eq→ i a') (eq→ i a)) - (distrib f) (distrib g)) - → f ≡ g - 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 private @@ -59,10 +42,9 @@ module _ (ℓ ℓ' : Level) where postulate eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''} → eq→ i (A ._⊕_ a' a) ≡ D ._⊕_ (eq→ i a') (eq→ i a)) (distrib (h ∘f (g ∘f f))) (distrib ((h ∘f g) ∘f f)) - -- eqD = {!!} assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f - assc = lift-eq-functors eq* eq→ eqI eqD + assc = Functor≡ eq* eq→ eqI eqD module _ {A B : Category ℓ ℓ'} {f : Functor A B} where lem : (func* f) ∘ (func* (identity {C = A})) ≡ func* f diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda index c0bebc1..e9ad7ce 100644 --- a/src/Cat/Functor.agda +++ b/src/Cat/Functor.agda @@ -19,9 +19,29 @@ record Functor {ℓc ℓc' ℓd ℓd'} (C : Category ℓc ℓc') (D : Category distrib : { c c' c'' : C .Object} {a : C .Arrow c c'} {a' : C .Arrow c' c''} → func→ (C ._⊕_ a' a) ≡ D ._⊕_ (func→ a') (func→ a) +open Functor +open Category + +module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where + private + _ℂ⊕_ = ℂ ._⊕_ + Functor≡ : {F G : Functor ℂ 𝔻} + → (eq* : F .func* ≡ G .func*) + → (eq→ : PathP (λ i → ∀ {x y} → ℂ .Arrow x y → 𝔻 .Arrow (eq* i x) (eq* i y)) + (F .func→) (G .func→)) + -- → (eq→ : Functor.func→ f ≡ {!!}) -- Functor.func→ g) + -- Use PathP + -- directly to show heterogeneous equalities by using previous + -- equalities (i.e. continuous paths) to create new continuous paths. + → (eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A}) + (ident F) (ident G)) + → (eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} + → eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f)) + (distrib F) (distrib G)) + → F ≡ G + Functor≡ eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; ident = eqI i ; distrib = eqD i } + module _ {ℓ ℓ' : Level} {A B C : Category ℓ ℓ'} (F : Functor B C) (G : Functor A B) where - open Functor - open Category private F* = F .func* F→ = F .func→ From 812662bda3bbb8e4fdd5bb5aac19ecb245020a9b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Thu, 25 Jan 2018 12:44:47 +0100 Subject: [PATCH 10/10] Rename some variables --- src/Cat/Categories/Cat.agda | 119 ++++++++++++++++++++---------------- src/Cat/Functor.agda | 12 ++-- 2 files changed, 72 insertions(+), 59 deletions(-) diff --git a/src/Cat/Categories/Cat.agda b/src/Cat/Categories/Cat.agda index f303937..4bac632 100644 --- a/src/Cat/Categories/Cat.agda +++ b/src/Cat/Categories/Cat.agda @@ -27,41 +27,62 @@ open Category 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) - eq* = refl - eq→ : PathP - (λ i → {x y : A .Object} → A .Arrow x y → D .Arrow (eq* i x) (eq* i y)) - (func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f)) - eq→ = refl - id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D - id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D - postulate eqI : PathP - (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ D .𝟙 {eq* i c}) - (ident ((h ∘f (g ∘f f)))) - (ident ((h ∘f g) ∘f f)) - postulate eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''} - → eq→ i (A ._⊕_ a' a) ≡ D ._⊕_ (eq→ i a') (eq→ i a)) - (distrib (h ∘f (g ∘f f))) (distrib ((h ∘f g) ∘f f)) + private + eq* : func* (h ∘f (g ∘f f)) ≡ func* ((h ∘f g) ∘f f) + eq* = refl + eq→ : PathP + (λ i → {x y : A .Object} → A .Arrow x y → D .Arrow (eq* i x) (eq* i y)) + (func→ (h ∘f (g ∘f f))) (func→ ((h ∘f g) ∘f f)) + eq→ = refl + id-l = (h ∘f (g ∘f f)) .ident -- = func→ (h ∘f (g ∘f f)) (𝟙 A) ≡ 𝟙 D + id-r = ((h ∘f g) ∘f f) .ident -- = func→ ((h ∘f g) ∘f f) (𝟙 A) ≡ 𝟙 D + postulate eqI : PathP + (λ i → ∀ {c : A .Object} → eq→ i (A .𝟙 {c}) ≡ D .𝟙 {eq* i c}) + (ident ((h ∘f (g ∘f f)))) + (ident ((h ∘f g) ∘f f)) + postulate eqD : PathP (λ i → { c c' c'' : A .Object} {a : A .Arrow c c'} {a' : A .Arrow c' c''} + → eq→ i (A ._⊕_ a' a) ≡ D ._⊕_ (eq→ i a') (eq→ i a)) + (distrib (h ∘f (g ∘f f))) (distrib ((h ∘f g) ∘f f)) assc : h ∘f (g ∘f f) ≡ (h ∘f g) ∘f f assc = Functor≡ eq* eq→ eqI eqD - module _ {A B : Category ℓ ℓ'} {f : Functor A B} where - lem : (func* f) ∘ (func* (identity {C = A})) ≡ func* f - lem = refl - -- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f - lemmm : PathP - (λ i → - {x y : Object A} → Arrow A x y → Arrow B (func* f x) (func* f y)) - (func→ (f ∘f identity)) (func→ f) - lemmm = refl - postulate lemz : PathP (λ i → {c : A .Object} → PathP (λ _ → Arrow B (func* f c) (func* f c)) (func→ f (A .𝟙)) (B .𝟙)) - (ident (f ∘f identity)) (ident f) - -- lemz = {!!} - postulate ident-r : f ∘f identity ≡ f - -- ident-r = lift-eq-functors lem lemmm {!lemz!} {!!} - postulate ident-l : identity ∘f f ≡ f - -- ident-l = lift-eq-functors lem lemmm {!refl!} {!!} + module _ {ℂ 𝔻 : Category ℓ ℓ'} {F : Functor ℂ 𝔻} where + module _ where + private + eq* : (func* F) ∘ (func* (identity {C = ℂ})) ≡ func* F + eq* = refl + -- lemmm : func→ {C = A} {D = B} (f ∘f identity) ≡ func→ f + eq→ : PathP + (λ i → + {x y : Object ℂ} → Arrow ℂ x y → Arrow 𝔻 (func* F x) (func* F y)) + (func→ (F ∘f identity)) (func→ F) + eq→ = refl + postulate + eqI-r : PathP (λ i → {c : ℂ .Object} + → PathP (λ _ → Arrow 𝔻 (func* F c) (func* F c)) (func→ F (ℂ .𝟙)) (𝔻 .𝟙)) + (ident (F ∘f identity)) (ident F) + eqD-r : PathP + (λ i → + {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} → + eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f)) + ((F ∘f identity) .distrib) (distrib F) + ident-r : F ∘f identity ≡ F + ident-r = Functor≡ eq* eq→ eqI-r eqD-r + module _ where + private + postulate + eq* : (identity ∘f F) .func* ≡ F .func* + eq→ : PathP + (λ i → {x y : Object ℂ} → ℂ .Arrow x y → 𝔻 .Arrow (eq* i x) (eq* i y)) + ((identity ∘f F) .func→) (F .func→) + eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A}) + (ident (identity ∘f F)) (ident F) + eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} + → eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f)) + (distrib (identity ∘f F)) (distrib F) + ident-l : identity ∘f F ≡ F + ident-l = Functor≡ eq* eq→ eqI eqD Cat : Category (lsuc (ℓ ⊔ ℓ')) (ℓ ⊔ ℓ') Cat = @@ -80,19 +101,19 @@ module _ (ℓ ℓ' : Level) where module _ {ℓ ℓ' : Level} where Catt = Cat ℓ ℓ' - module _ (C D : Category ℓ ℓ') where + module _ (ℂ 𝔻 : Category ℓ ℓ') where private - :Object: = C .Object × D .Object + :Object: = ℂ .Object × 𝔻 .Object :Arrow: : :Object: → :Object: → Set ℓ' - :Arrow: (c , d) (c' , d') = Arrow C c c' × Arrow D d d' + :Arrow: (c , d) (c' , d') = Arrow ℂ c c' × Arrow 𝔻 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} + _:⊕:_ = λ { (bc∈C , bc∈D) (ab∈C , ab∈D) → (ℂ ._⊕_) bc∈C ab∈C , 𝔻 ._⊕_ bc∈D ab∈D} instance :isCategory: : IsCategory :Object: :Arrow: :𝟙: _:⊕:_ @@ -103,8 +124,8 @@ module _ {ℓ ℓ' : Level} where , eqpair (snd C.ident) (snd D.ident) } where - open module C = IsCategory (C .isCategory) - open module D = IsCategory (D .isCategory) + open module C = IsCategory (ℂ .isCategory) + open module D = IsCategory (𝔻 .isCategory) :product: : Category ℓ ℓ' :product: = record @@ -114,13 +135,13 @@ module _ {ℓ ℓ' : Level} where ; _⊕_ = _:⊕:_ } - proj₁ : Arrow Catt :product: C + proj₁ : Arrow Catt :product: ℂ proj₁ = record { func* = fst ; func→ = fst ; ident = refl ; distrib = refl } - proj₂ : Arrow Catt :product: D + proj₂ : Arrow Catt :product: 𝔻 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 + module _ {X : Object Catt} (x₁ : Arrow Catt X ℂ) (x₂ : Arrow Catt X 𝔻) where open Functor -- ident' : {c : Object X} → ((func→ x₁) {dom = c} (𝟙 X) , (func→ x₂) {dom = c} (𝟙 X)) ≡ 𝟙 (catProduct C D) @@ -137,10 +158,10 @@ module _ {ℓ ℓ' : Level} where -- 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 {!!} {!!} + -- isUniqL = Functor≡ refl refl {!!} {!!} postulate isUniqR : (Catt ⊕ proj₂) x ≡ x₂ - -- isUniqR = lift-eq-functors refl refl {!!} {!!} + -- isUniqR = Functor≡ refl refl {!!} {!!} isUniq : (Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂ isUniq = isUniqL , isUniqR @@ -148,11 +169,11 @@ module _ {ℓ ℓ' : Level} where uniq : ∃![ x ] ((Catt ⊕ proj₁) x ≡ x₁ × (Catt ⊕ proj₂) x ≡ x₂) uniq = x , isUniq - instance - isProduct : IsProduct Catt proj₁ proj₂ - isProduct = uniq + instance + isProduct : IsProduct (Cat ℓ ℓ') proj₁ proj₂ + isProduct = uniq - product : Product {ℂ = Catt} C D + product : Product {ℂ = (Cat ℓ ℓ')} ℂ 𝔻 product = record { obj = :product: ; proj₁ = proj₁ @@ -160,7 +181,6 @@ module _ {ℓ ℓ' : Level} where } module _ {ℓ ℓ' : Level} where - open Category instance hasProducts : HasProducts (Cat ℓ ℓ') hasProducts = record { product = product } @@ -169,9 +189,7 @@ module _ {ℓ ℓ' : Level} where module _ (ℓ : Level) where private open Data.Product - open Category open import Cat.Categories.Fun - open Functor Catℓ : Category (lsuc (ℓ ⊔ ℓ)) (ℓ ⊔ ℓ) Catℓ = Cat ℓ ℓ @@ -317,7 +335,6 @@ module _ (ℓ : Level) where catTranspose : ∃![ F~ ] (Catℓ ._⊕_ :eval: (parallelProduct F~ (Catℓ .𝟙 {o = ℂ})) ≡ F) catTranspose = transpose , eq - -- :isExponential: : IsExponential Catℓ A B :obj: {!:eval:!} :isExponential: : IsExponential Catℓ ℂ 𝔻 :obj: :eval: :isExponential: = catTranspose diff --git a/src/Cat/Functor.agda b/src/Cat/Functor.agda index e9ad7ce..919ef22 100644 --- a/src/Cat/Functor.agda +++ b/src/Cat/Functor.agda @@ -28,16 +28,12 @@ module _ {ℓ ℓ' : Level} {ℂ 𝔻 : Category ℓ ℓ'} where Functor≡ : {F G : Functor ℂ 𝔻} → (eq* : F .func* ≡ G .func*) → (eq→ : PathP (λ i → ∀ {x y} → ℂ .Arrow x y → 𝔻 .Arrow (eq* i x) (eq* i y)) - (F .func→) (G .func→)) - -- → (eq→ : Functor.func→ f ≡ {!!}) -- Functor.func→ g) - -- Use PathP - -- directly to show heterogeneous equalities by using previous - -- equalities (i.e. continuous paths) to create new continuous paths. + (F .func→) (G .func→)) → (eqI : PathP (λ i → ∀ {A : ℂ .Object} → eq→ i (ℂ .𝟙 {A}) ≡ 𝔻 .𝟙 {eq* i A}) - (ident F) (ident G)) + (ident F) (ident G)) → (eqD : PathP (λ i → {A B C : ℂ .Object} {f : ℂ .Arrow A B} {g : ℂ .Arrow B C} - → eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f)) - (distrib F) (distrib G)) + → eq→ i (ℂ ._⊕_ g f) ≡ 𝔻 ._⊕_ (eq→ i g) (eq→ i f)) + (distrib F) (distrib G)) → F ≡ G Functor≡ eq* eq→ eqI eqD i = record { func* = eq* i ; func→ = eq→ i ; ident = eqI i ; distrib = eqD i }