From ff5ff5699bf2c484dfd935ef439276a79b148269 Mon Sep 17 00:00:00 2001 From: bond15 Date: Wed, 8 May 2024 19:17:17 +0000 Subject: [PATCH 01/10] coend base --- .../Categories/Constructions/Coend/Base.agda | 104 ++++++++++++++++++ 1 file changed, 104 insertions(+) create mode 100644 Cubical/Categories/Constructions/Coend/Base.agda diff --git a/Cubical/Categories/Constructions/Coend/Base.agda b/Cubical/Categories/Constructions/Coend/Base.agda new file mode 100644 index 00000000..600c8d8c --- /dev/null +++ b/Cubical/Categories/Constructions/Coend/Base.agda @@ -0,0 +1,104 @@ +{-# OPTIONS --allow-unsolved-metas #-} +-- following 1 Lab +-- https://1lab.dev/Cat.Diagram.Coend.Sets.html + +module Cubical.Categories.Constructions.Coend.Base where + open import Cubical.Categories.Bifunctor.Base + open import Cubical.Categories.Category + open import Cubical.Categories.Functor + open import Cubical.Categories.Instances.Sets + + open import Cubical.Foundations.HLevels + open import Cubical.Foundations.Prelude + + private + variable + ℓC ℓC' ℓD ℓD' : Level + + module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D)where + + open Category C renaming (ob to obᶜ ; _⋆_ to _⋆ᶜ_ ; id to idᶜ) + open Category D renaming (ob to obᵈ ; _⋆_ to _⋆ᵈ_ ; id to idᵈ) + + record Cowedge : Set (ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD'))) where + field + nadir : obᵈ + ψ : (c : obᶜ) → D [ F ⟅ c , c ⟆b , nadir ] + {- + for all morphisms f : c ⇒ c' in category C, + + F₀(c',c)---F₁(id(c'),f)---> F₀(c',c') + | | + F₁(f,id(c)) ψ(c') + ↓ ↓ + F₀(c,c)---ψ(c)-----------> nadir + -} + extranatural : {c c' : obᶜ}(f : C [ c , c' ]) → + (F ⟪ idᶜ , f ⟫lr ⋆ᵈ ψ c') ≡ ( F ⟪ f , idᶜ ⟫lr ⋆ᵈ ψ c) + + record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD')))) where + open Cowedge + field + cowedge : Cowedge + factor : (W : Cowedge ) → D [ cowedge .nadir , W .nadir ] + commutes : (W : Cowedge )(c : obᶜ) → (cowedge .ψ c ⋆ᵈ factor W) ≡ W .ψ c + unique : (W : Cowedge )(factor' : D [ cowedge .nadir , W .nadir ]) → + (∀(c : obᶜ) → (cowedge .ψ c ⋆ᵈ factor') ≡ W .ψ c) → + factor' ≡ factor W + + module _ {C : Category ℓC ℓC'}(F : Bifunctor (C ^op) C (SET (ℓ-max ℓC ℓC')) ) where + open import Cubical.HITs.SetCoequalizer + open Category + + Set-Coend : Coend F + Set-Coend = coend where + open Cowedge + open Coend + + lmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) + → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) + lmap (X , Y , f , Fxy ) = X , ( F ⟪ id C {X} , f ⟫lr ) Fxy + + rmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) + → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) + rmap (X , Y , f , Fxy ) = Y , ( F ⟪ f , id C {Y} ⟫lr ) Fxy + + {- + for morphism f : Y ⇒ X in category C, + + -- this diagram is just the coeq constructor + + F₀(X , Y)---rmap---> Σ[ X ∈ ob C] F (X , X) + | | + lmap inc + | | + Σ[ X ∈ ob C] F (X , X)---inc-----> SetCoequalizer lmap rmap + -} + + univ : Cowedge F + univ .nadir = SetCoequalizer lmap rmap , squash + univ .ψ X Fxx = inc (X , Fxx) + univ .extranatural {Y} {X} f = funExt λ Fxy → coeq (X , Y , f , Fxy) + + open UniversalProperty using (inducedHom ; uniqueness) + factoring : (W : Cowedge F) → SetCoequalizer lmap rmap → fst (W .nadir) + factoring W = + inducedHom + (W .nadir .snd) + (λ {(x , Fxx) → W .ψ x Fxx}) + λ{(X , Y , f , Fxy) → funExt⁻ (W .extranatural f) Fxy} + + coend : Coend F + coend .cowedge = univ + coend .factor = factoring + coend .commutes W c = refl + coend .unique W factor' commutes' = + -- uniqueness here follows from uniqueness of maps out of the coequalizer + uniqueness + lmap + rmap + (W .nadir .snd) + (λ{ (c , Fcc) → W . ψ c Fcc}) + (λ{( X , Y , f , Fxy ) → funExt⁻ (W .extranatural f) Fxy }) + factor' + λ{(x , Fxx) → funExt⁻ (sym(commutes' x)) Fxx} \ No newline at end of file From 8416af7d37b7d31591bfb5b25c795c7ee4b4b229 Mon Sep 17 00:00:00 2001 From: bond15 Date: Wed, 8 May 2024 19:18:46 +0000 Subject: [PATCH 02/10] bifunctor syntax --- Cubical/Categories/Bifunctor/Base.agda | 7 ++ Cubical/Categories/Coend/Base.agda | 104 +++++++++++++++++++++++++ 2 files changed, 111 insertions(+) create mode 100644 Cubical/Categories/Coend/Base.agda diff --git a/Cubical/Categories/Bifunctor/Base.agda b/Cubical/Categories/Bifunctor/Base.agda index ced03c80..d5015c7d 100644 --- a/Cubical/Categories/Bifunctor/Base.agda +++ b/Cubical/Categories/Bifunctor/Base.agda @@ -89,6 +89,13 @@ _⟪_⟫r : (F : Bifunctor C D E) → E [(F ⟅ c , d ⟆b) , (F ⟅ c , d' ⟆b)] F ⟪ f ⟫r = Bif-homR F _ f +_⟪_,_⟫lr : (F : Bifunctor C D E) + → ∀ {c c' d d'} + → C [ c , c' ] + → D [ d , d' ] + → E [(F ⟅ c , d ⟆b) , (F ⟅ c' , d' ⟆b)] +_⟪_,_⟫lr {E = E} F f g = F ⟪ f ⟫l ⋆⟨ E ⟩ F ⟪ g ⟫r + Fst : Bifunctor C D C Fst .Bif-ob = λ z _ → z Fst .Bif-homL = λ z d → z diff --git a/Cubical/Categories/Coend/Base.agda b/Cubical/Categories/Coend/Base.agda new file mode 100644 index 00000000..68669708 --- /dev/null +++ b/Cubical/Categories/Coend/Base.agda @@ -0,0 +1,104 @@ +{-# OPTIONS --allow-unsolved-metas #-} +-- following 1 Lab +-- https://1lab.dev/Cat.Diagram.Coend.Sets.html + +module Cubical.Categories.Coend.Base where + open import Cubical.Categories.Bifunctor.Base + open import Cubical.Categories.Category + open import Cubical.Categories.Functor + open import Cubical.Categories.Instances.Sets + + open import Cubical.Foundations.HLevels + open import Cubical.Foundations.Prelude + + private + variable + ℓC ℓC' ℓD ℓD' : Level + + module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D)where + + open Category C renaming (ob to obᶜ ; _⋆_ to _⋆ᶜ_ ; id to idᶜ) + open Category D renaming (ob to obᵈ ; _⋆_ to _⋆ᵈ_ ; id to idᵈ) + + record Cowedge : Set (ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD'))) where + field + nadir : obᵈ + ψ : (c : obᶜ) → D [ F ⟅ c , c ⟆b , nadir ] + {- + for all morphisms f : c ⇒ c' in category C, + + F₀(c',c)---F₁(id(c'),f)---> F₀(c',c') + | | + F₁(f,id(c)) ψ(c') + ↓ ↓ + F₀(c,c)---ψ(c)-----------> nadir + -} + extranatural : {c c' : obᶜ}(f : C [ c , c' ]) → + (F ⟪ idᶜ , f ⟫lr ⋆ᵈ ψ c') ≡ ( F ⟪ f , idᶜ ⟫lr ⋆ᵈ ψ c) + + record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD')))) where + open Cowedge + field + cowedge : Cowedge + factor : (W : Cowedge ) → D [ cowedge .nadir , W .nadir ] + commutes : (W : Cowedge )(c : obᶜ) → (cowedge .ψ c ⋆ᵈ factor W) ≡ W .ψ c + unique : (W : Cowedge )(factor' : D [ cowedge .nadir , W .nadir ]) → + (∀(c : obᶜ) → (cowedge .ψ c ⋆ᵈ factor') ≡ W .ψ c) → + factor' ≡ factor W + + module _ {C : Category ℓC ℓC'}(F : Bifunctor (C ^op) C (SET (ℓ-max ℓC ℓC')) ) where + open import Cubical.HITs.SetCoequalizer + open Category + + Set-Coend : Coend F + Set-Coend = coend where + open Cowedge + open Coend + + lmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) + → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) + lmap (X , Y , f , Fxy ) = X , ( F ⟪ id C {X} , f ⟫lr ) Fxy + + rmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) + → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) + rmap (X , Y , f , Fxy ) = Y , ( F ⟪ f , id C {Y} ⟫lr ) Fxy + + {- + for morphism f : Y ⇒ X in category C, + + -- this diagram is just the coeq constructor + + F₀(X , Y)---rmap---> Σ[ X ∈ ob C] F (X , X) + | | + lmap inc + | | + Σ[ X ∈ ob C] F (X , X)---inc-----> SetCoequalizer lmap rmap + -} + + univ : Cowedge F + univ .nadir = SetCoequalizer lmap rmap , squash + univ .ψ X Fxx = inc (X , Fxx) + univ .extranatural {Y} {X} f = funExt λ Fxy → coeq (X , Y , f , Fxy) + + open UniversalProperty using (inducedHom ; uniqueness) + factoring : (W : Cowedge F) → SetCoequalizer lmap rmap → fst (W .nadir) + factoring W = + inducedHom + (W .nadir .snd) + (λ {(x , Fxx) → W .ψ x Fxx}) + λ{(X , Y , f , Fxy) → funExt⁻ (W .extranatural f) Fxy} + + coend : Coend F + coend .cowedge = univ + coend .factor = factoring + coend .commutes W c = refl + coend .unique W factor' commutes' = + -- uniqueness here follows from uniqueness of maps out of the coequalizer + uniqueness + lmap + rmap + (W .nadir .snd) + (λ{ (c , Fcc) → W . ψ c Fcc}) + (λ{( X , Y , f , Fxy ) → funExt⁻ (W .extranatural f) Fxy }) + factor' + λ{(x , Fxx) → funExt⁻ (sym(commutes' x)) Fxx} \ No newline at end of file From 15c794649f25da9b44b9286b6516d5f890047986 Mon Sep 17 00:00:00 2001 From: bond15 Date: Wed, 8 May 2024 19:20:17 +0000 Subject: [PATCH 03/10] remove redundancy --- Cubical/Categories/Coend/Base.agda | 104 ----------------------------- 1 file changed, 104 deletions(-) delete mode 100644 Cubical/Categories/Coend/Base.agda diff --git a/Cubical/Categories/Coend/Base.agda b/Cubical/Categories/Coend/Base.agda deleted file mode 100644 index 68669708..00000000 --- a/Cubical/Categories/Coend/Base.agda +++ /dev/null @@ -1,104 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} --- following 1 Lab --- https://1lab.dev/Cat.Diagram.Coend.Sets.html - -module Cubical.Categories.Coend.Base where - open import Cubical.Categories.Bifunctor.Base - open import Cubical.Categories.Category - open import Cubical.Categories.Functor - open import Cubical.Categories.Instances.Sets - - open import Cubical.Foundations.HLevels - open import Cubical.Foundations.Prelude - - private - variable - ℓC ℓC' ℓD ℓD' : Level - - module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D)where - - open Category C renaming (ob to obᶜ ; _⋆_ to _⋆ᶜ_ ; id to idᶜ) - open Category D renaming (ob to obᵈ ; _⋆_ to _⋆ᵈ_ ; id to idᵈ) - - record Cowedge : Set (ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD'))) where - field - nadir : obᵈ - ψ : (c : obᶜ) → D [ F ⟅ c , c ⟆b , nadir ] - {- - for all morphisms f : c ⇒ c' in category C, - - F₀(c',c)---F₁(id(c'),f)---> F₀(c',c') - | | - F₁(f,id(c)) ψ(c') - ↓ ↓ - F₀(c,c)---ψ(c)-----------> nadir - -} - extranatural : {c c' : obᶜ}(f : C [ c , c' ]) → - (F ⟪ idᶜ , f ⟫lr ⋆ᵈ ψ c') ≡ ( F ⟪ f , idᶜ ⟫lr ⋆ᵈ ψ c) - - record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD')))) where - open Cowedge - field - cowedge : Cowedge - factor : (W : Cowedge ) → D [ cowedge .nadir , W .nadir ] - commutes : (W : Cowedge )(c : obᶜ) → (cowedge .ψ c ⋆ᵈ factor W) ≡ W .ψ c - unique : (W : Cowedge )(factor' : D [ cowedge .nadir , W .nadir ]) → - (∀(c : obᶜ) → (cowedge .ψ c ⋆ᵈ factor') ≡ W .ψ c) → - factor' ≡ factor W - - module _ {C : Category ℓC ℓC'}(F : Bifunctor (C ^op) C (SET (ℓ-max ℓC ℓC')) ) where - open import Cubical.HITs.SetCoequalizer - open Category - - Set-Coend : Coend F - Set-Coend = coend where - open Cowedge - open Coend - - lmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) - → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) - lmap (X , Y , f , Fxy ) = X , ( F ⟪ id C {X} , f ⟫lr ) Fxy - - rmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) - → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) - rmap (X , Y , f , Fxy ) = Y , ( F ⟪ f , id C {Y} ⟫lr ) Fxy - - {- - for morphism f : Y ⇒ X in category C, - - -- this diagram is just the coeq constructor - - F₀(X , Y)---rmap---> Σ[ X ∈ ob C] F (X , X) - | | - lmap inc - | | - Σ[ X ∈ ob C] F (X , X)---inc-----> SetCoequalizer lmap rmap - -} - - univ : Cowedge F - univ .nadir = SetCoequalizer lmap rmap , squash - univ .ψ X Fxx = inc (X , Fxx) - univ .extranatural {Y} {X} f = funExt λ Fxy → coeq (X , Y , f , Fxy) - - open UniversalProperty using (inducedHom ; uniqueness) - factoring : (W : Cowedge F) → SetCoequalizer lmap rmap → fst (W .nadir) - factoring W = - inducedHom - (W .nadir .snd) - (λ {(x , Fxx) → W .ψ x Fxx}) - λ{(X , Y , f , Fxy) → funExt⁻ (W .extranatural f) Fxy} - - coend : Coend F - coend .cowedge = univ - coend .factor = factoring - coend .commutes W c = refl - coend .unique W factor' commutes' = - -- uniqueness here follows from uniqueness of maps out of the coequalizer - uniqueness - lmap - rmap - (W .nadir .snd) - (λ{ (c , Fcc) → W . ψ c Fcc}) - (λ{( X , Y , f , Fxy ) → funExt⁻ (W .extranatural f) Fxy }) - factor' - λ{(x , Fxx) → funExt⁻ (sym(commutes' x)) Fxx} \ No newline at end of file From 20830c01bf36f365477e5c8e92f5a477b29d2aa7 Mon Sep 17 00:00:00 2001 From: bond15 Date: Thu, 9 May 2024 00:41:53 +0000 Subject: [PATCH 04/10] --safe flag --- Cubical/Categories/Constructions/Coend/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cubical/Categories/Constructions/Coend/Base.agda b/Cubical/Categories/Constructions/Coend/Base.agda index 600c8d8c..22571f71 100644 --- a/Cubical/Categories/Constructions/Coend/Base.agda +++ b/Cubical/Categories/Constructions/Coend/Base.agda @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --safe #-} -- following 1 Lab -- https://1lab.dev/Cat.Diagram.Coend.Sets.html From b368f018a16a6315d6e76060d442468b8e7db568 Mon Sep 17 00:00:00 2001 From: bond15 Date: Sat, 25 May 2024 01:59:55 +0000 Subject: [PATCH 05/10] forgot to add syntax level --- Cubical/Categories/Bifunctor/Base.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Cubical/Categories/Bifunctor/Base.agda b/Cubical/Categories/Bifunctor/Base.agda index d5015c7d..f4b5f9e2 100644 --- a/Cubical/Categories/Bifunctor/Base.agda +++ b/Cubical/Categories/Bifunctor/Base.agda @@ -77,6 +77,9 @@ infix 30 _⟪_⟫l infix 30 _⟪_⟫r -- same infix level as on objects since these will -- never be used in the same context +infix 30 _⟪_,_⟫lr +-- same infix level as on objects since these will +-- never be used in the same context _⟪_⟫l : (F : Bifunctor C D E) → ∀ {c c' d} → C [ c , c' ] From d901e955ce619e992e04fba72a5f02639df3d74e Mon Sep 17 00:00:00 2001 From: bond15 Date: Sat, 25 May 2024 02:09:26 +0000 Subject: [PATCH 06/10] converting to module syntax --- Cubical/Categories/Constructions/Coend/Base.agda | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Cubical/Categories/Constructions/Coend/Base.agda b/Cubical/Categories/Constructions/Coend/Base.agda index 22571f71..c2c644ad 100644 --- a/Cubical/Categories/Constructions/Coend/Base.agda +++ b/Cubical/Categories/Constructions/Coend/Base.agda @@ -17,13 +17,13 @@ module Cubical.Categories.Constructions.Coend.Base where module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D)where - open Category C renaming (ob to obᶜ ; _⋆_ to _⋆ᶜ_ ; id to idᶜ) - open Category D renaming (ob to obᵈ ; _⋆_ to _⋆ᵈ_ ; id to idᵈ) + module C = Category C + module D = Category D record Cowedge : Set (ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD'))) where field - nadir : obᵈ - ψ : (c : obᶜ) → D [ F ⟅ c , c ⟆b , nadir ] + nadir : D.ob + ψ : (c : C.ob) → D [ F ⟅ c , c ⟆b , nadir ] {- for all morphisms f : c ⇒ c' in category C, @@ -33,17 +33,17 @@ module Cubical.Categories.Constructions.Coend.Base where ↓ ↓ F₀(c,c)---ψ(c)-----------> nadir -} - extranatural : {c c' : obᶜ}(f : C [ c , c' ]) → - (F ⟪ idᶜ , f ⟫lr ⋆ᵈ ψ c') ≡ ( F ⟪ f , idᶜ ⟫lr ⋆ᵈ ψ c) + extranatural : {c c' : C.ob}(f : C [ c , c' ]) → + (F ⟪ C.id , f ⟫lr D.⋆ ψ c') ≡ ( F ⟪ f , C.id ⟫lr D.⋆ ψ c) record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD')))) where open Cowedge field cowedge : Cowedge factor : (W : Cowedge ) → D [ cowedge .nadir , W .nadir ] - commutes : (W : Cowedge )(c : obᶜ) → (cowedge .ψ c ⋆ᵈ factor W) ≡ W .ψ c + commutes : (W : Cowedge )(c : C.ob) → (cowedge .ψ c D.⋆ factor W) ≡ W .ψ c unique : (W : Cowedge )(factor' : D [ cowedge .nadir , W .nadir ]) → - (∀(c : obᶜ) → (cowedge .ψ c ⋆ᵈ factor') ≡ W .ψ c) → + (∀(c : C.ob) → (cowedge .ψ c D.⋆ factor') ≡ W .ψ c) → factor' ≡ factor W module _ {C : Category ℓC ℓC'}(F : Bifunctor (C ^op) C (SET (ℓ-max ℓC ℓC')) ) where From 5bd2365dcd8607564225244ab9cce742b88d5206 Mon Sep 17 00:00:00 2001 From: bond15 Date: Sat, 25 May 2024 02:15:35 +0000 Subject: [PATCH 07/10] fix-whitespace --- .../Categories/Constructions/Coend/Base.agda | 64 +++++++++---------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/Cubical/Categories/Constructions/Coend/Base.agda b/Cubical/Categories/Constructions/Coend/Base.agda index c2c644ad..3a6e8211 100644 --- a/Cubical/Categories/Constructions/Coend/Base.agda +++ b/Cubical/Categories/Constructions/Coend/Base.agda @@ -2,7 +2,7 @@ -- following 1 Lab -- https://1lab.dev/Cat.Diagram.Coend.Sets.html -module Cubical.Categories.Constructions.Coend.Base where +module Cubical.Categories.Constructions.Coend.Base where open import Cubical.Categories.Bifunctor.Base open import Cubical.Categories.Category open import Cubical.Categories.Functor @@ -17,41 +17,41 @@ module Cubical.Categories.Constructions.Coend.Base where module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D)where - module C = Category C + module C = Category C module D = Category D - record Cowedge : Set (ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD'))) where - field + record Cowedge : Set (ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD'))) where + field nadir : D.ob ψ : (c : C.ob) → D [ F ⟅ c , c ⟆b , nadir ] - {- + {- for all morphisms f : c ⇒ c' in category C, F₀(c',c)---F₁(id(c'),f)---> F₀(c',c') | | F₁(f,id(c)) ψ(c') - ↓ ↓ + ↓ ↓ F₀(c,c)---ψ(c)-----------> nadir -} - extranatural : {c c' : C.ob}(f : C [ c , c' ]) → + extranatural : {c c' : C.ob}(f : C [ c , c' ]) → (F ⟪ C.id , f ⟫lr D.⋆ ψ c') ≡ ( F ⟪ f , C.id ⟫lr D.⋆ ψ c) - - record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD')))) where + + record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD')))) where open Cowedge - field + field cowedge : Cowedge factor : (W : Cowedge ) → D [ cowedge .nadir , W .nadir ] commutes : (W : Cowedge )(c : C.ob) → (cowedge .ψ c D.⋆ factor W) ≡ W .ψ c - unique : (W : Cowedge )(factor' : D [ cowedge .nadir , W .nadir ]) → - (∀(c : C.ob) → (cowedge .ψ c D.⋆ factor') ≡ W .ψ c) → + unique : (W : Cowedge )(factor' : D [ cowedge .nadir , W .nadir ]) → + (∀(c : C.ob) → (cowedge .ψ c D.⋆ factor') ≡ W .ψ c) → factor' ≡ factor W module _ {C : Category ℓC ℓC'}(F : Bifunctor (C ^op) C (SET (ℓ-max ℓC ℓC')) ) where - open import Cubical.HITs.SetCoequalizer - open Category - - Set-Coend : Coend F - Set-Coend = coend where + open import Cubical.HITs.SetCoequalizer + open Category + + Set-Coend : Coend F + Set-Coend = coend where open Cowedge open Coend @@ -62,11 +62,11 @@ module Cubical.Categories.Constructions.Coend.Base where rmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) rmap (X , Y , f , Fxy ) = Y , ( F ⟪ f , id C {Y} ⟫lr ) Fxy - - {- + + {- for morphism f : Y ⇒ X in category C, - -- this diagram is just the coeq constructor + -- this diagram is just the coeq constructor F₀(X , Y)---rmap---> Σ[ X ∈ ob C] F (X , X) | | @@ -75,30 +75,30 @@ module Cubical.Categories.Constructions.Coend.Base where Σ[ X ∈ ob C] F (X , X)---inc-----> SetCoequalizer lmap rmap -} - univ : Cowedge F + univ : Cowedge F univ .nadir = SetCoequalizer lmap rmap , squash univ .ψ X Fxx = inc (X , Fxx) univ .extranatural {Y} {X} f = funExt λ Fxy → coeq (X , Y , f , Fxy) open UniversalProperty using (inducedHom ; uniqueness) factoring : (W : Cowedge F) → SetCoequalizer lmap rmap → fst (W .nadir) - factoring W = - inducedHom - (W .nadir .snd) - (λ {(x , Fxx) → W .ψ x Fxx}) + factoring W = + inducedHom + (W .nadir .snd) + (λ {(x , Fxx) → W .ψ x Fxx}) λ{(X , Y , f , Fxy) → funExt⁻ (W .extranatural f) Fxy} coend : Coend F coend .cowedge = univ coend .factor = factoring coend .commutes W c = refl - coend .unique W factor' commutes' = + coend .unique W factor' commutes' = -- uniqueness here follows from uniqueness of maps out of the coequalizer - uniqueness + uniqueness lmap - rmap - (W .nadir .snd) - (λ{ (c , Fcc) → W . ψ c Fcc}) + rmap + (W .nadir .snd) + (λ{ (c , Fcc) → W . ψ c Fcc}) (λ{( X , Y , f , Fxy ) → funExt⁻ (W .extranatural f) Fxy }) - factor' - λ{(x , Fxx) → funExt⁻ (sym(commutes' x)) Fxx} \ No newline at end of file + factor' + λ{(x , Fxx) → funExt⁻ (sym(commutes' x)) Fxx} From f8e25aefed58ad3e6b9af5da0a9e925ca4672ed1 Mon Sep 17 00:00:00 2001 From: bond15 Date: Sat, 25 May 2024 02:31:46 +0000 Subject: [PATCH 08/10] adding TODO, starting to fix line length --- Cubical/Categories/Constructions/Coend/Base.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Cubical/Categories/Constructions/Coend/Base.agda b/Cubical/Categories/Constructions/Coend/Base.agda index 3a6e8211..701c60df 100644 --- a/Cubical/Categories/Constructions/Coend/Base.agda +++ b/Cubical/Categories/Constructions/Coend/Base.agda @@ -15,7 +15,7 @@ module Cubical.Categories.Constructions.Coend.Base where variable ℓC ℓC' ℓD ℓD' : Level - module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D)where + module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D) where module C = Category C module D = Category D @@ -36,6 +36,8 @@ module Cubical.Categories.Constructions.Coend.Base where extranatural : {c c' : C.ob}(f : C [ c , c' ]) → (F ⟪ C.id , f ⟫lr D.⋆ ψ c') ≡ ( F ⟪ f , C.id ⟫lr D.⋆ ψ c) + -- TODO : Can probably define a Presheaf structure for Cowedge + -- and then this should be isomorphic to a universal element of that presheaf. record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD')))) where open Cowedge field From 57b705bf9a66c129f919c4d11939c89fce581450 Mon Sep 17 00:00:00 2001 From: bond15 Date: Sat, 25 May 2024 02:41:39 +0000 Subject: [PATCH 09/10] fix whitespace and line length --- .../Categories/Constructions/Coend/Base.agda | 43 ++++++++++++------- 1 file changed, 28 insertions(+), 15 deletions(-) diff --git a/Cubical/Categories/Constructions/Coend/Base.agda b/Cubical/Categories/Constructions/Coend/Base.agda index 701c60df..0f2d1bd6 100644 --- a/Cubical/Categories/Constructions/Coend/Base.agda +++ b/Cubical/Categories/Constructions/Coend/Base.agda @@ -15,7 +15,9 @@ module Cubical.Categories.Constructions.Coend.Base where variable ℓC ℓC' ℓD ℓD' : Level - module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}(F : Bifunctor (C ^op) C D) where + module _ {C : Category ℓC ℓC'} + {D : Category ℓD ℓD'} + (F : Bifunctor (C ^op) C D) where module C = Category C module D = Category D @@ -36,19 +38,23 @@ module Cubical.Categories.Constructions.Coend.Base where extranatural : {c c' : C.ob}(f : C [ c , c' ]) → (F ⟪ C.id , f ⟫lr D.⋆ ψ c') ≡ ( F ⟪ f , C.id ⟫lr D.⋆ ψ c) - -- TODO : Can probably define a Presheaf structure for Cowedge - -- and then this should be isomorphic to a universal element of that presheaf. + -- TODO : Can probably define a Presheaf structure for Cowedge and then + -- this should be isomorphic to a universal element of that presheaf. record Coend : Set ((ℓ-max ℓC (ℓ-max ℓC' (ℓ-max ℓD ℓD')))) where open Cowedge field cowedge : Cowedge factor : (W : Cowedge ) → D [ cowedge .nadir , W .nadir ] - commutes : (W : Cowedge )(c : C.ob) → (cowedge .ψ c D.⋆ factor W) ≡ W .ψ c - unique : (W : Cowedge )(factor' : D [ cowedge .nadir , W .nadir ]) → - (∀(c : C.ob) → (cowedge .ψ c D.⋆ factor') ≡ W .ψ c) → - factor' ≡ factor W - - module _ {C : Category ℓC ℓC'}(F : Bifunctor (C ^op) C (SET (ℓ-max ℓC ℓC')) ) where + commutes : (W : Cowedge ) + (c : C.ob) → + (cowedge .ψ c D.⋆ factor W) ≡ W .ψ c + unique : (W : Cowedge ) + (factor' : D [ cowedge .nadir , W .nadir ]) → + (∀(c : C.ob) → (cowedge .ψ c D.⋆ factor') ≡ W .ψ c) → + factor' ≡ factor W + + module _ {C : Category ℓC ℓC'} + (F : Bifunctor (C ^op) C (SET (ℓ-max ℓC ℓC')) ) where open import Cubical.HITs.SetCoequalizer open Category @@ -57,12 +63,16 @@ module Cubical.Categories.Constructions.Coend.Base where open Cowedge open Coend - lmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) - → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) + lmap : Σ[ X ∈ ob C ] + Σ[ Y ∈ ob C ] + Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) + → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) lmap (X , Y , f , Fxy ) = X , ( F ⟪ id C {X} , f ⟫lr ) Fxy - rmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) - → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) + rmap : Σ[ X ∈ ob C ] + Σ[ Y ∈ ob C ] + Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) + → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) rmap (X , Y , f , Fxy ) = Y , ( F ⟪ f , id C {Y} ⟫lr ) Fxy {- @@ -83,7 +93,9 @@ module Cubical.Categories.Constructions.Coend.Base where univ .extranatural {Y} {X} f = funExt λ Fxy → coeq (X , Y , f , Fxy) open UniversalProperty using (inducedHom ; uniqueness) - factoring : (W : Cowedge F) → SetCoequalizer lmap rmap → fst (W .nadir) + factoring : (W : Cowedge F) → + SetCoequalizer lmap rmap → + fst (W .nadir) factoring W = inducedHom (W .nadir .snd) @@ -95,7 +107,8 @@ module Cubical.Categories.Constructions.Coend.Base where coend .factor = factoring coend .commutes W c = refl coend .unique W factor' commutes' = - -- uniqueness here follows from uniqueness of maps out of the coequalizer + -- uniqueness here follows from + -- uniqueness of maps out of the coequalizer uniqueness lmap rmap From 0224c7c23609d6663fcaacfd8a2d16718df23df4 Mon Sep 17 00:00:00 2001 From: bond15 Date: Sat, 3 Aug 2024 14:50:53 +0000 Subject: [PATCH 10/10] use redundant bifunctor --- Cubical/Categories/Bifunctor/Base.agda | 10 ---------- Cubical/Categories/Constructions/Coend/Base.agda | 8 ++++---- 2 files changed, 4 insertions(+), 14 deletions(-) diff --git a/Cubical/Categories/Bifunctor/Base.agda b/Cubical/Categories/Bifunctor/Base.agda index f4b5f9e2..ced03c80 100644 --- a/Cubical/Categories/Bifunctor/Base.agda +++ b/Cubical/Categories/Bifunctor/Base.agda @@ -77,9 +77,6 @@ infix 30 _⟪_⟫l infix 30 _⟪_⟫r -- same infix level as on objects since these will -- never be used in the same context -infix 30 _⟪_,_⟫lr --- same infix level as on objects since these will --- never be used in the same context _⟪_⟫l : (F : Bifunctor C D E) → ∀ {c c' d} → C [ c , c' ] @@ -92,13 +89,6 @@ _⟪_⟫r : (F : Bifunctor C D E) → E [(F ⟅ c , d ⟆b) , (F ⟅ c , d' ⟆b)] F ⟪ f ⟫r = Bif-homR F _ f -_⟪_,_⟫lr : (F : Bifunctor C D E) - → ∀ {c c' d d'} - → C [ c , c' ] - → D [ d , d' ] - → E [(F ⟅ c , d ⟆b) , (F ⟅ c' , d' ⟆b)] -_⟪_,_⟫lr {E = E} F f g = F ⟪ f ⟫l ⋆⟨ E ⟩ F ⟪ g ⟫r - Fst : Bifunctor C D C Fst .Bif-ob = λ z _ → z Fst .Bif-homL = λ z d → z diff --git a/Cubical/Categories/Constructions/Coend/Base.agda b/Cubical/Categories/Constructions/Coend/Base.agda index 0f2d1bd6..930ad89b 100644 --- a/Cubical/Categories/Constructions/Coend/Base.agda +++ b/Cubical/Categories/Constructions/Coend/Base.agda @@ -3,7 +3,7 @@ -- https://1lab.dev/Cat.Diagram.Coend.Sets.html module Cubical.Categories.Constructions.Coend.Base where - open import Cubical.Categories.Bifunctor.Base + open import Cubical.Categories.Bifunctor.Redundant open import Cubical.Categories.Category open import Cubical.Categories.Functor open import Cubical.Categories.Instances.Sets @@ -36,7 +36,7 @@ module Cubical.Categories.Constructions.Coend.Base where F₀(c,c)---ψ(c)-----------> nadir -} extranatural : {c c' : C.ob}(f : C [ c , c' ]) → - (F ⟪ C.id , f ⟫lr D.⋆ ψ c') ≡ ( F ⟪ f , C.id ⟫lr D.⋆ ψ c) + (F ⟪ C.id , f ⟫× D.⋆ ψ c') ≡ ( F ⟪ f , C.id ⟫× D.⋆ ψ c) -- TODO : Can probably define a Presheaf structure for Cowedge and then -- this should be isomorphic to a universal element of that presheaf. @@ -67,13 +67,13 @@ module Cubical.Categories.Constructions.Coend.Base where Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) - lmap (X , Y , f , Fxy ) = X , ( F ⟪ id C {X} , f ⟫lr ) Fxy + lmap (X , Y , f , Fxy ) = X , ( F ⟪ id C {X} , f ⟫× ) Fxy rmap : Σ[ X ∈ ob C ] Σ[ Y ∈ ob C ] Σ[ f ∈ (C)[ Y , X ] ] fst( F ⟅ X , Y ⟆b ) → Σ[ X ∈ ob C ] fst ( F ⟅ X , X ⟆b) - rmap (X , Y , f , Fxy ) = Y , ( F ⟪ f , id C {Y} ⟫lr ) Fxy + rmap (X , Y , f , Fxy ) = Y , ( F ⟪ f , id C {Y} ⟫× ) Fxy {- for morphism f : Y ⇒ X in category C,