From 8f725398c3f284e868f196777a32e290fd855c2a Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Thu, 29 May 2025 13:06:18 -0400 Subject: [PATCH 01/20] Dualize cones, limits, right (kan) extensions --- .../cocones-precategories.lagda.md | 302 ++++++++++++++++++ .../colimits-precategories.lagda.md | 266 +++++++++++++++ .../coproducts-in-precategories.lagda.md | 36 +++ .../left-extensions-precategories.lagda.md | 250 +++++++++++++++ ...left-kan-extensions-precategories.lagda.md | 94 ++++++ 5 files changed, 948 insertions(+) create mode 100644 src/category-theory/cocones-precategories.lagda.md create mode 100644 src/category-theory/colimits-precategories.lagda.md create mode 100644 src/category-theory/left-extensions-precategories.lagda.md create mode 100644 src/category-theory/left-kan-extensions-precategories.lagda.md diff --git a/src/category-theory/cocones-precategories.lagda.md b/src/category-theory/cocones-precategories.lagda.md new file mode 100644 index 0000000000..57db7bd856 --- /dev/null +++ b/src/category-theory/cocones-precategories.lagda.md @@ -0,0 +1,302 @@ +# Cocones in precategories + +```agda +module category-theory.cocones-precategories where +``` + +
Imports + +```agda +open import category-theory.commuting-squares-of-morphisms-in-precategories +open import category-theory.commuting-triangles-of-morphisms-in-precategories +open import category-theory.constant-functors +open import category-theory.functors-precategories +open import category-theory.left-extensions-precategories +open import category-theory.maps-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.precategories +open import category-theory.precategory-of-functors +open import category-theory.terminal-category + +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-identifications +open import foundation.dependent-pair-types +open import foundation.equality-dependent-function-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.multivariable-homotopies +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.sets +open import foundation.structure-identity-principle +open import foundation.torsorial-type-families +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +A +{{#concept "cocone" Disambiguation="over a functor between precategories" Agda=cocone-Precategory}} +over a [functor](category-theory.functors-precategories.md) `F` between +[precategories](category-theory.precategories.md) is a +[natural transformation](category-theory.natural-transformations-functors-precategories.md) +from a [constant functor](category-theory.constant-functors.md) to `F`. + +In this context, we usually think of (and refer to) the functor `F` as a +**diagram** in its codomain, A cocone over such diagram then corresponds to an +element `d`, called the **vertex** of the cocone, equipped with components +`d → F x` satisfying the naturality condition. + +For example, if `F` corresponds to the diagram `F x → F y`, then a cocone over +`F` corresponds to a commuting triangle as below. + +```text + d + / \ + / \ + ∨ ∨ + Fx ----> Fy +``` + +Equivalently, we can see a cocone over `F` as a +[right extension](category-theory.right-extensions-precategories.md) of `F` +along the terminal functor into the +[terminal precategory](category-theory.terminal-category.md). + +## Definitions + +### The type of cocones over a functor + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + where + + cocone-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + cocone-Precategory = + Σ ( obj-Precategory D) + ( λ d → + natural-transformation-Precategory C D + ( F) + ( constant-functor-Precategory C D d)) + + make-cocone-Precategory : + ( d : obj-Precategory D) + ( α : + ( x : obj-Precategory C) → + ( hom-Precategory D (obj-functor-Precategory C D F x) d)) → + ( {x y : obj-Precategory C} (f : hom-Precategory C x y) → + coherence-triangle-hom-Precategory D + ( hom-functor-Precategory C D F f) + ( α x) + ( α y)) → + cocone-Precategory + pr1 (make-cocone-Precategory d α p) = d + pr1 (pr2 (make-cocone-Precategory d α p)) = α + pr2 (pr2 (make-cocone-Precategory d α p)) f = + left-unit-law-comp-hom-Precategory D _ ∙ p f + + vertex-cocone-Precategory : cocone-Precategory → obj-Precategory D + vertex-cocone-Precategory = pr1 + + vertex-functor-cocone-Precategory : + cocone-Precategory → functor-Precategory C D + vertex-functor-cocone-Precategory α = + constant-functor-Precategory C D (vertex-cocone-Precategory α) + + natural-transformation-cocone-Precategory : + (α : cocone-Precategory) → + natural-transformation-Precategory C D + ( F) + ( vertex-functor-cocone-Precategory α) + natural-transformation-cocone-Precategory = pr2 + + component-cocone-Precategory : + (α : cocone-Precategory) (x : obj-Precategory C) → + hom-Precategory D + ( obj-functor-Precategory C D F x) + ( vertex-cocone-Precategory α) + component-cocone-Precategory α = + hom-family-natural-transformation-Precategory C D + ( F) + ( vertex-functor-cocone-Precategory α) + ( natural-transformation-cocone-Precategory α) + + naturality-cocone-Precategory : + (α : cocone-Precategory) {x y : obj-Precategory C} + (f : hom-Precategory C x y) → + coherence-triangle-hom-Precategory D + ( hom-functor-Precategory C D F f) + ( component-cocone-Precategory α x) + ( component-cocone-Precategory α y) + naturality-cocone-Precategory α {x} {y} f = + inv (left-unit-law-comp-hom-Precategory D _) ∙ + naturality-natural-transformation-Precategory C D + ( F) + ( vertex-functor-cocone-Precategory α) + ( natural-transformation-cocone-Precategory α) + ( f) +``` + +### Postcomposing cocones + +```agda + cocone-map-Precategory : + (τ : cocone-Precategory) + (d : obj-Precategory D) → + (hom-Precategory D (vertex-cocone-Precategory τ) d) → + natural-transformation-Precategory C D + ( F) + ( constant-functor-Precategory C D d) + pr1 (cocone-map-Precategory τ d f) x = + comp-hom-Precategory D f (component-cocone-Precategory τ x) + pr2 (cocone-map-Precategory τ d f) h = + left-unit-law-comp-hom-Precategory D _ ∙ + ap + ( λ g → comp-hom-Precategory D f g) + ( naturality-cocone-Precategory τ h) ∙ + inv (associative-comp-hom-Precategory D _ _ _) +``` + +## Properties + +### Characterization of equality of cocones over functors between precategories + +```agda + coherence-htpy-cocone-Precategory : + (α β : cocone-Precategory) → + (p : vertex-cocone-Precategory α ＝ vertex-cocone-Precategory β) → + UU (l1 ⊔ l4) + coherence-htpy-cocone-Precategory α β p = + (x : obj-Precategory C) → + coherence-triangle-hom-Precategory D + ( component-cocone-Precategory α x) + ( component-cocone-Precategory β x) + ( hom-eq-Precategory D + ( vertex-cocone-Precategory α) + ( vertex-cocone-Precategory β) + ( p)) + + htpy-cocone-Precategory : + (α β : cocone-Precategory) → + UU (l1 ⊔ l3 ⊔ l4) + htpy-cocone-Precategory α β = + Σ ( vertex-cocone-Precategory α ＝ vertex-cocone-Precategory β) + ( coherence-htpy-cocone-Precategory α β) + + refl-htpy-cocone-Precategory : + (α : cocone-Precategory) → + htpy-cocone-Precategory α α + pr1 (refl-htpy-cocone-Precategory α) = refl + pr2 (refl-htpy-cocone-Precategory α) x = + inv (left-unit-law-comp-hom-Precategory D _) + + htpy-eq-cocone-Precategory : + (α β : cocone-Precategory) → + α ＝ β → + htpy-cocone-Precategory α β + htpy-eq-cocone-Precategory α .α refl = refl-htpy-cocone-Precategory α + + is-torsorial-htpy-cocone-Precategory : + (α : cocone-Precategory) → + is-torsorial (htpy-cocone-Precategory α) + is-torsorial-htpy-cocone-Precategory α = + is-torsorial-Eq-structure + ( is-torsorial-Id (vertex-cocone-Precategory α)) + ( pair (vertex-cocone-Precategory α) refl) + ( is-contr-equiv + ( Σ + ( natural-transformation-Precategory C D + F (constant-functor-Precategory C D (vertex-cocone-Precategory α))) + (λ τ → τ ＝ (natural-transformation-cocone-Precategory α))) + ( equiv-tot + ( λ τ → + inv-equiv + ( extensionality-natural-transformation-Precategory C D + ( F) + ( constant-functor-Precategory C D + ( vertex-cocone-Precategory α)) + ( _) + ( _)) ∘e + equiv-Π-equiv-family + ( λ x → + equiv-concat' + ( pr1 τ x) + ( left-unit-law-comp-hom-Precategory D _)))) + ( is-torsorial-Id' (natural-transformation-cocone-Precategory α))) + + is-equiv-htpy-eq-cocone-Precategory : + (α β : cocone-Precategory) → + is-equiv (htpy-eq-cocone-Precategory α β) + is-equiv-htpy-eq-cocone-Precategory α = + fundamental-theorem-id + ( is-torsorial-htpy-cocone-Precategory α) + ( htpy-eq-cocone-Precategory α) + + equiv-htpy-eq-cocone-Precategory : + (α β : cocone-Precategory) → + (α ＝ β) ≃ htpy-cocone-Precategory α β + pr1 (equiv-htpy-eq-cocone-Precategory α β) = htpy-eq-cocone-Precategory α β + pr2 (equiv-htpy-eq-cocone-Precategory α β) = + is-equiv-htpy-eq-cocone-Precategory α β + + eq-htpy-cocone-Precategory : + (α β : cocone-Precategory) → + htpy-cocone-Precategory α β → + α ＝ β + eq-htpy-cocone-Precategory α β = + map-inv-equiv (equiv-htpy-eq-cocone-Precategory α β) +``` + +### A cocone is a left extension along the terminal map + +```agda + equiv-left-extension-cocone-Precategory : + cocone-Precategory ≃ + left-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F + equiv-left-extension-cocone-Precategory = + equiv-Σ-equiv-base + ( λ K → natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C terminal-Precategory D + ( K) + ( terminal-functor-Precategory C))) + ( equiv-point-Precategory D) + + left-extension-cocone-Precategory : + cocone-Precategory → + left-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F + left-extension-cocone-Precategory = + map-equiv equiv-left-extension-cocone-Precategory + + cocone-left-extension-Precategory : + left-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F → + cocone-Precategory + cocone-left-extension-Precategory = + map-inv-equiv equiv-left-extension-cocone-Precategory + + vertex-left-extension-Precategory : + left-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F → + obj-Precategory D + vertex-left-extension-Precategory R = + vertex-cocone-Precategory + ( cocone-left-extension-Precategory R) +``` diff --git a/src/category-theory/colimits-precategories.lagda.md b/src/category-theory/colimits-precategories.lagda.md new file mode 100644 index 0000000000..a96236e62a --- /dev/null +++ b/src/category-theory/colimits-precategories.lagda.md @@ -0,0 +1,266 @@ +# Colimits in precategories + +```agda +module category-theory.colimits-precategories where +``` + +
Imports + +```agda +open import category-theory.cocones-precategories +open import category-theory.constant-functors +open import category-theory.functors-precategories +open import category-theory.left-extensions-precategories +open import category-theory.left-kan-extensions-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.precategories +open import category-theory.terminal-category + +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.identity-types +open import foundation.logical-equivalences +open import foundation.propositions +open import foundation.transport-along-identifications +open import foundation.unit-type +open import foundation.universe-levels +``` + +
+ +## Idea + +A +{{#concept "colimit" Disambiguation="of a functor of precategories" Agda=colimit-Precategory}} +of a [functor](category-theory.functors-precategories.md) `F` between +[precategories](category-theory.precategories.md) is a colimiting +[cocone](category-theory.cocones-precategories.md) under `F`. That is, a cocone +`τ` such that `cocone-map-Precategory C D F τ d` is an equivalence for all +`d : obj-Precategory D`. + +Equivalently, the colimit of `F` is a +[left kan extension](category-theory.left-kan-extensions-precategories.md) of +`F` along the terminal functor into the +[terminal precategory](category-theory.terminal-category.md). + +We show that both definitions coincide, and we will use the definition using +colimiting cocones as our official one. + +If a colimit exists, we call the vertex of the colimiting cocone the **vertex** +of the colimit. + +## Definition + +### Colimiting cocones + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + where + + is-colimiting-cocone-Precategory : + cocone-Precategory C D F → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-colimiting-cocone-Precategory τ = + (d : obj-Precategory D) → + is-equiv (cocone-map-Precategory C D F τ d) + + colimit-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + colimit-Precategory = + Σ ( cocone-Precategory C D F) + ( is-colimiting-cocone-Precategory) + + cocone-colimit-Precategory : + colimit-Precategory → + cocone-Precategory C D F + cocone-colimit-Precategory = pr1 + + vertex-colimit-Precategory : + colimit-Precategory → + obj-Precategory D + vertex-colimit-Precategory τ = + vertex-cocone-Precategory C D F (cocone-colimit-Precategory τ) + + is-colimiting-colimit-Precategory : + (τ : colimit-Precategory) → + is-colimiting-cocone-Precategory (cocone-colimit-Precategory τ) + is-colimiting-colimit-Precategory = pr2 + + hom-cocone-colimit-Precategory : + (τ : colimit-Precategory) → + (φ : cocone-Precategory C D F) → + hom-Precategory D + ( vertex-colimit-Precategory τ) + ( vertex-cocone-Precategory C D F φ) + hom-cocone-colimit-Precategory τ φ = + map-inv-is-equiv + ( is-colimiting-colimit-Precategory τ + ( vertex-cocone-Precategory C D F φ)) + ( natural-transformation-cocone-Precategory C D F φ) +``` + +### Colimits through left kan extensions + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + where + + is-colimit-left-extension-Precategory : + left-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F → + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + is-colimit-left-extension-Precategory = + is-left-kan-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F + + colimit-Precategory' : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) + colimit-Precategory' = + left-kan-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F + +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) (L : colimit-Precategory' C D F) + where + + left-extension-colimit-Precategory' : + left-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F + left-extension-colimit-Precategory' = + left-extension-left-kan-extension-Precategory + C terminal-Precategory D (terminal-functor-Precategory C) F L + + extension-colimit-Precategory' : + functor-Precategory terminal-Precategory D + extension-colimit-Precategory' = + extension-left-kan-extension-Precategory + C terminal-Precategory D (terminal-functor-Precategory C) F L +``` + +## Properties + +### Being a colimit is a property + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + where + + is-prop-is-colimiting-cocone-Precategory : + (τ : cocone-Precategory C D F) → + is-prop (is-colimiting-cocone-Precategory C D F τ) + is-prop-is-colimiting-cocone-Precategory τ = + is-prop-Π λ φ → is-property-is-equiv _ + + is-prop-is-colimit-Precategory' : + ( R : left-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F) → + is-prop (is-colimit-left-extension-Precategory C D F R) + is-prop-is-colimit-Precategory' R = + is-prop-Π λ K → is-property-is-equiv _ +``` + +### Colimiting cocones are equivalent to colimits + +```agda +module _ + {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + where + + equiv-is-left-kan-extension-is-colimiting-Precategory : + (τ : cocone-Precategory C D F) → + is-colimiting-cocone-Precategory C D F τ ≃ + is-left-kan-extension-Precategory C terminal-Precategory D + (terminal-functor-Precategory C) F + (map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) + equiv-is-left-kan-extension-is-colimiting-Precategory τ = + equiv-Π _ + ( equiv-point-Precategory D) + ( λ x → + equiv-iff-is-prop + ( is-property-is-equiv _) + ( is-property-is-equiv _) + ( λ e → + is-equiv-left-factor + ( induced-left-extension-map x) + ( natural-transformation-constant-functor-Precategory + terminal-Precategory D) + ( tr is-equiv (inv (lemma τ x)) e) + ( is-equiv-natural-transformation-constant-functor-Precategory + D _ _)) + ( λ e → + tr is-equiv (lemma τ x) + ( is-equiv-comp + ( induced-left-extension-map x) + ( natural-transformation-constant-functor-Precategory + terminal-Precategory D) + ( is-equiv-natural-transformation-constant-functor-Precategory + D _ _) + ( e)))) + where + induced-left-extension-map = λ x → + left-extension-map-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) ( F) + ( map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) + ( constant-functor-Precategory terminal-Precategory D x) + lemma : + ( τ : cocone-Precategory C D F) + ( x : obj-Precategory D) → + ( left-extension-map-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) F + ( map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) + ( constant-functor-Precategory terminal-Precategory D x)) ∘ + ( natural-transformation-constant-functor-Precategory + terminal-Precategory D) ＝ + ( cocone-map-Precategory C D F τ x) + lemma τ x = + eq-htpy λ f → + eq-htpy-hom-family-natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C terminal-Precategory D + ( point-Precategory D x) + ( terminal-functor-Precategory C)) + ( _) + ( _) + ( λ g → refl) + + equiv-colimit-colimit'-Precategory : + colimit-Precategory C D F ≃ colimit-Precategory' C D F + equiv-colimit-colimit'-Precategory = + equiv-Σ + ( is-left-kan-extension-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) F) + ( equiv-left-extension-cocone-Precategory C D F) + ( λ τ → equiv-is-left-kan-extension-is-colimiting-Precategory τ) + + colimit-colimit'-Precategory : + colimit-Precategory C D F → colimit-Precategory' C D F + colimit-colimit'-Precategory = + map-equiv equiv-colimit-colimit'-Precategory + + colimit'-colimit-Precategory : + colimit-Precategory' C D F → colimit-Precategory C D F + colimit'-colimit-Precategory = + map-inv-equiv equiv-colimit-colimit'-Precategory +``` + +### Existence of colimits + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + has-colimits-Precategory : (l3 l4 : Level) → UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ lsuc l4) + has-colimits-Precategory l3 l4 = + (J : Precategory l3 l4) → (F : functor-Precategory J C) → + colimit-Precategory J C F +``` diff --git a/src/category-theory/coproducts-in-precategories.lagda.md b/src/category-theory/coproducts-in-precategories.lagda.md index cc72f57907..bb682ae009 100644 --- a/src/category-theory/coproducts-in-precategories.lagda.md +++ b/src/category-theory/coproducts-in-precategories.lagda.md @@ -16,6 +16,7 @@ open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.iterated-dependent-product-types open import foundation.propositions +open import foundation.sets open import foundation.uniqueness-quantification open import foundation.universe-levels ``` @@ -156,3 +157,38 @@ module _ (comp-hom-Precategory C (inl-coproduct-obj-Precategory C t y₁ y₂) f) (comp-hom-Precategory C (inr-coproduct-obj-Precategory C t y₁ y₂) g) ``` + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + is-coproduct-set-obj-Precategory : + {l : Level} (S : Set l) + (I : type-Set S → obj-Precategory C) → + (c : obj-Precategory C) + (ι : (i : type-Set S) → hom-Precategory C (I i) c) → + UU (l1 ⊔ l2 ⊔ l) + is-coproduct-set-obj-Precategory S I c ι = + (z : obj-Precategory C) → + (f : (i : type-Set S) → hom-Precategory C (I i) z) → + ( uniquely-exists-structure + ( hom-Precategory C c z) + ( λ h → + (i : type-Set S) → + ( comp-hom-Precategory C h (ι i)) ＝ f i)) + + coproduct-set-obj-Precategory : + {l : Level} (S : Set l) + (I : type-Set S → obj-Precategory C) → + UU (l1 ⊔ l2 ⊔ l) + coproduct-set-obj-Precategory S I = + Σ (obj-Precategory C) λ c → + Σ ((i : type-Set S) → hom-Precategory C (I i) c) λ ι → + is-coproduct-set-obj-Precategory S I c ι + + has-all-coproducts-Precategory : (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) + has-all-coproducts-Precategory l = + (S : Set l) (I : type-Set S → obj-Precategory C) → + coproduct-set-obj-Precategory S I +``` diff --git a/src/category-theory/left-extensions-precategories.lagda.md b/src/category-theory/left-extensions-precategories.lagda.md new file mode 100644 index 0000000000..1214b92702 --- /dev/null +++ b/src/category-theory/left-extensions-precategories.lagda.md @@ -0,0 +1,250 @@ +# Left extensions in precategories + +```agda +module category-theory.left-extensions-precategories where +``` + +
Imports + +```agda +open import category-theory.functors-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.precategories + +open import foundation.action-on-equivalences-functions +open import foundation.action-on-identifications-functions +open import foundation.contractible-types +open import foundation.dependent-identifications +open import foundation.dependent-pair-types +open import foundation.equality-dependent-function-types +open import foundation.equality-dependent-pair-types +open import foundation.equivalences +open import foundation.function-extensionality +open import foundation.function-types +open import foundation.functoriality-dependent-pair-types +open import foundation.fundamental-theorem-of-identity-types +open import foundation.homotopies +open import foundation.homotopy-induction +open import foundation.identity-types +open import foundation.multivariable-homotopies +open import foundation.propositions +open import foundation.retractions +open import foundation.sections +open import foundation.sets +open import foundation.structure-identity-principle +open import foundation.torsorial-type-families +open import foundation.unit-type +open import foundation.universe-levels + +open import foundation-core.functoriality-dependent-function-types +``` + +
+ +## Idea + +A +{{#concept "left extension" Disambiguation="of a functor between precategories" Agda=left-extension-Precategory}} +of a [functor](category-theory.functors-precategories.md) `F : C → D` between +[precategories](category-theory.precategories.md) along another functor +`p : C → C'` is a functor `G : C' → D` together with a +[natural transformation](category-theory.natural-transformations-functors-precategories.md) +`φ : F → G ∘ p`. + +```text + C + | \ + p F + | \ + ∨ ∨ + C' - G -> D +``` + +We note that this is not a standard definition, but it inspired by the notion of +a [left kan extension](category-theory.left-kan-extensions-precategories.md). + +## Definition + +### Left extensions + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (C : Precategory l1 l2) (C' : Precategory l3 l4) (D : Precategory l5 l6) + (p : functor-Precategory C C') (F : functor-Precategory C D) + where + + left-extension-Precategory : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + left-extension-Precategory = + Σ ( functor-Precategory C' D) + ( λ G → + natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D G p)) + + module _ + (L : left-extension-Precategory) + where + + extension-left-extension-Precategory : functor-Precategory C' D + extension-left-extension-Precategory = pr1 L + + natural-transformation-left-extension-Precategory : + natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + ( extension-left-extension-Precategory) + ( p)) + natural-transformation-left-extension-Precategory = pr2 L + + hom-family-left-extension-Precategory : + hom-family-functor-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + ( extension-left-extension-Precategory) + ( p)) + hom-family-left-extension-Precategory = + hom-family-natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + ( extension-left-extension-Precategory) + ( p)) + ( natural-transformation-left-extension-Precategory) + + naturality-left-extension-Precategory : + is-natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + ( extension-left-extension-Precategory) + ( p)) + ( hom-family-left-extension-Precategory) + naturality-left-extension-Precategory = + naturality-natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + ( extension-left-extension-Precategory) + ( p)) + ( natural-transformation-left-extension-Precategory) +``` + +### Postcomposing left extensions + +```agda + left-extension-map-Precategory : + ( G : functor-Precategory C' D) → + ( natural-transformation-Precategory C' D + extension-left-extension-Precategory G) → + ( natural-transformation-Precategory C D + F ( comp-functor-Precategory C C' D G p)) + left-extension-map-Precategory G φ = + comp-natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + extension-left-extension-Precategory p) + ( comp-functor-Precategory C C' D G p) + ( right-whisker-natural-transformation-Precategory C' D C + ( extension-left-extension-Precategory) + ( G) + ( φ) + ( p)) + ( natural-transformation-left-extension-Precategory) +``` + +## Properties + +### Characterization of equality left extensions of functors between precategories + +```agda + coherence-htpy-left-extension-Precategory : + (R S : left-extension-Precategory) + (e : + (extension-left-extension-Precategory R) ＝ + (extension-left-extension-Precategory S)) → + UU (l1 ⊔ l6) + coherence-htpy-left-extension-Precategory R S e = + (x : obj-Precategory C) → + comp-hom-Precategory D + ( hom-family-natural-transformation-Precategory C' D (pr1 R) (pr1 S) + ( natural-transformation-eq-Precategory C' D + ( extension-left-extension-Precategory R) + ( extension-left-extension-Precategory S) + ( e)) + ( obj-functor-Precategory C C' p x)) + ( hom-family-left-extension-Precategory R x) ＝ + hom-family-left-extension-Precategory S x + + htpy-left-extension-Precategory : + (R S : left-extension-Precategory) → + UU (l1 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + htpy-left-extension-Precategory R S = + Σ ( extension-left-extension-Precategory R ＝ + extension-left-extension-Precategory S) + ( coherence-htpy-left-extension-Precategory R S) + + is-torsorial-htpy-left-extension-Precategory : + (R : left-extension-Precategory) → + is-torsorial (htpy-left-extension-Precategory R) + is-torsorial-htpy-left-extension-Precategory R = + is-torsorial-Eq-structure + ( is-torsorial-Id (extension-left-extension-Precategory R)) + ( pair (extension-left-extension-Precategory R) refl) + ( is-contr-equiv + ( Σ + ( natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + ( extension-left-extension-Precategory R) p)) + ( λ τ → τ ＝ natural-transformation-left-extension-Precategory R)) + ( equiv-tot + ( λ τ → + inv-equiv + ( extensionality-natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + ( extension-left-extension-Precategory R) p) + _ _) ∘e + equiv-Π-equiv-family + ( λ x → + equiv-inv _ _ ∘e + equiv-inv-concat (left-unit-law-comp-hom-Precategory D _) _))) + ( is-torsorial-Id' + ( natural-transformation-left-extension-Precategory R))) + + refl-htpy-left-extension-Precategory : + (R : left-extension-Precategory) → + htpy-left-extension-Precategory R R + pr1 (refl-htpy-left-extension-Precategory R) = refl + pr2 (refl-htpy-left-extension-Precategory R) x = + left-unit-law-comp-hom-Precategory D _ + + htpy-eq-left-extension-Precategory : + (R S : left-extension-Precategory) → + R ＝ S → + htpy-left-extension-Precategory R S + htpy-eq-left-extension-Precategory R .R refl = + refl-htpy-left-extension-Precategory R + + is-equiv-htpy-eq-left-extension-Precategory : + (R S : left-extension-Precategory) → + is-equiv (htpy-eq-left-extension-Precategory R S) + is-equiv-htpy-eq-left-extension-Precategory R = + fundamental-theorem-id + ( is-torsorial-htpy-left-extension-Precategory R) + ( htpy-eq-left-extension-Precategory R) + + equiv-htpy-eq-left-extension-Precategory : + (R S : left-extension-Precategory) → + (R ＝ S) ≃ htpy-left-extension-Precategory R S + pr1 (equiv-htpy-eq-left-extension-Precategory R S) = + htpy-eq-left-extension-Precategory R S + pr2 (equiv-htpy-eq-left-extension-Precategory R S) = + is-equiv-htpy-eq-left-extension-Precategory R S + + eq-htpy-left-extension-Precategory : + (R S : left-extension-Precategory) → + htpy-left-extension-Precategory R S → + R ＝ S + eq-htpy-left-extension-Precategory R S = + map-inv-equiv (equiv-htpy-eq-left-extension-Precategory R S) +``` diff --git a/src/category-theory/left-kan-extensions-precategories.lagda.md b/src/category-theory/left-kan-extensions-precategories.lagda.md new file mode 100644 index 0000000000..9f23b81ffc --- /dev/null +++ b/src/category-theory/left-kan-extensions-precategories.lagda.md @@ -0,0 +1,94 @@ +# Left Kan extensions in precategories + +```agda +module category-theory.left-kan-extensions-precategories where +``` + +
Imports + +```agda +open import category-theory.functors-precategories +open import category-theory.left-extensions-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.precategories + +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +A +{{#concept "left Kan extension" Disambiguation="of a functor between precategories" Agda=is-left-kan-extension-Precategory}} +of [functor](category-theory.functors-precategories.md) `F : C → D` between +[precategories](category-theory.precategories.md) along another functor +`p : C → C'` is the universal +[left extension](category-theory.left-extensions-precategories.md) of `F` along +`p`. + +More concretely, we require the function `left-extension-map-Precategory` to be +an equivalence. + +## Definition + +```agda +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (C : Precategory l1 l2) (C' : Precategory l3 l4) (D : Precategory l5 l6) + (p : functor-Precategory C C') (F : functor-Precategory C D) + (R : left-extension-Precategory C C' D p F) + where + + is-left-kan-extension-Precategory : + UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + is-left-kan-extension-Precategory = + ( G : functor-Precategory C' D) → + is-equiv (left-extension-map-Precategory C C' D p F R G) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (C : Precategory l1 l2) (C' : Precategory l3 l4) (D : Precategory l5 l6) + (p : functor-Precategory C C') (F : functor-Precategory C D) + where + + left-kan-extension-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6) + left-kan-extension-Precategory = + Σ ( left-extension-Precategory C C' D p F) + ( is-left-kan-extension-Precategory C C' D p F) + +module _ + {l1 l2 l3 l4 l5 l6 : Level} + (C : Precategory l1 l2) (C' : Precategory l3 l4) (D : Precategory l5 l6) + (p : functor-Precategory C C') (F : functor-Precategory C D) + (R : left-kan-extension-Precategory C C' D p F) + where + + left-extension-left-kan-extension-Precategory : + left-extension-Precategory C C' D p F + left-extension-left-kan-extension-Precategory = pr1 R + + is-left-kan-extension-left-kan-extension-Precategory : + is-left-kan-extension-Precategory C C' D p F (pr1 R) + is-left-kan-extension-left-kan-extension-Precategory = pr2 R + + extension-left-kan-extension-Precategory : + functor-Precategory C' D + extension-left-kan-extension-Precategory = + extension-left-extension-Precategory C C' D p F + left-extension-left-kan-extension-Precategory + + natural-transformation-left-kan-extension-Precategory : + natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C C' D + ( extension-left-extension-Precategory C C' D p F + left-extension-left-kan-extension-Precategory) + ( p)) + natural-transformation-left-kan-extension-Precategory = + natural-transformation-left-extension-Precategory C C' D p F + left-extension-left-kan-extension-Precategory +``` From 7ab6863d2b4b4dbd302e0a0278d81d85a9d77c17 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Mon, 9 Jun 2025 11:52:39 -0400 Subject: [PATCH 02/20] Explicitly dualize monads --- src/category-theory.lagda.md | 5 + ...lgebras-comonads-on-precategories.lagda.md | 101 ++++ .../comonads-on-precategories.lagda.md | 448 ++++++++++++++++++ ...ointed-endofunctors-precategories.lagda.md | 142 ++++++ .../monads-on-precategories.lagda.md | 6 +- ...lgebras-comonads-on-precategories.lagda.md | 121 +++++ ...lgebras-comonads-on-precategories.lagda.md | 357 ++++++++++++++ 7 files changed, 1177 insertions(+), 3 deletions(-) create mode 100644 src/category-theory/coalgebras-comonads-on-precategories.lagda.md create mode 100644 src/category-theory/comonads-on-precategories.lagda.md create mode 100644 src/category-theory/copointed-endofunctors-precategories.lagda.md create mode 100644 src/category-theory/morphisms-coalgebras-comonads-on-precategories.lagda.md create mode 100644 src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index 4e78e73234..0a145482ef 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -25,16 +25,19 @@ open import category-theory.category-of-functors public open import category-theory.category-of-functors-from-small-to-large-categories public open import category-theory.category-of-maps-categories public open import category-theory.category-of-maps-from-small-to-large-categories public +open import category-theory.coalgebras-comonads-on-precategories public open import category-theory.commuting-squares-of-morphisms-in-large-precategories public open import category-theory.commuting-squares-of-morphisms-in-precategories public open import category-theory.commuting-squares-of-morphisms-in-set-magmoids public open import category-theory.commuting-triangles-of-morphisms-in-precategories public open import category-theory.commuting-triangles-of-morphisms-in-set-magmoids public +open import category-theory.comonads-on-precategories public open import category-theory.complete-precategories public open import category-theory.composition-operations-on-binary-families-of-sets public open import category-theory.cones-precategories public open import category-theory.conservative-functors-precategories public open import category-theory.constant-functors public +open import category-theory.copointed-endofunctors-precategories public open import category-theory.copresheaf-categories public open import category-theory.coproducts-in-precategories public open import category-theory.cores-categories public @@ -111,6 +114,7 @@ open import category-theory.monads-on-categories public open import category-theory.monads-on-precategories public open import category-theory.monomorphisms-in-large-precategories public open import category-theory.morphisms-algebras-monads-on-precategories public +open import category-theory.morphisms-coalgebras-comonads-on-precategories public open import category-theory.natural-isomorphisms-functors-categories public open import category-theory.natural-isomorphisms-functors-large-precategories public open import category-theory.natural-isomorphisms-functors-precategories public @@ -137,6 +141,7 @@ open import category-theory.pointed-endofunctors-categories public open import category-theory.pointed-endofunctors-precategories public open import category-theory.precategories public open import category-theory.precategory-of-algebras-monads-on-precategories public +open import category-theory.precategory-of-coalgebras-comonads-on-precategories public open import category-theory.precategory-of-elements-of-a-presheaf public open import category-theory.precategory-of-free-algebras-monads-on-precategories public open import category-theory.precategory-of-functors public diff --git a/src/category-theory/coalgebras-comonads-on-precategories.lagda.md b/src/category-theory/coalgebras-comonads-on-precategories.lagda.md new file mode 100644 index 0000000000..663ac55d77 --- /dev/null +++ b/src/category-theory/coalgebras-comonads-on-precategories.lagda.md @@ -0,0 +1,101 @@ +# Coalgebras over comonads on precategories + +```agda +module category-theory.coalgebras-comonads-on-precategories where +``` + +
Imports + +```agda +open import category-theory.commuting-squares-of-morphisms-in-precategories +open import category-theory.comonads-on-precategories +open import category-theory.functors-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.natural-transformations-maps-precategories +open import category-theory.precategories + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.sets +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +``` + +
+ +## Idea + +A +{{#concept "coalgebra" Disambiguation="over a comonad on a precategory" Agda=coalgebra-comonad-Precategory}} +over a [comonad](category-theory.comonads-on-precategories.md) `T` consists of +an object `A` and morphism `a : A → TA` satisfying two compatibility laws: + +- **Counit law**: `ε_A ∘ a = id_A` +- **Comultiplication law**: `Ta ∘ a = δ ∘ a` + +## Definitions + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : comonad-Precategory C) + where + + module _ + {A : obj-Precategory C} + (a : hom-Precategory C A (obj-endofunctor-comonad-Precategory C T A)) + where + + has-counit-law-coalgebra-comonad-Precategory : UU l2 + has-counit-law-coalgebra-comonad-Precategory = + comp-hom-Precategory C (hom-counit-comonad-Precategory C T A) a ＝ + id-hom-Precategory C + + has-comul-law-coalgebra-comonad-Precategory : UU l2 + has-comul-law-coalgebra-comonad-Precategory = + comp-hom-Precategory C (hom-endofunctor-comonad-Precategory C T a) a ＝ + comp-hom-Precategory C (hom-comul-comonad-Precategory C T A) a + + is-coalgebra-comonad-Precategory : UU l2 + is-coalgebra-comonad-Precategory = + has-counit-law-coalgebra-comonad-Precategory × + has-comul-law-coalgebra-comonad-Precategory + + coalgebra-comonad-Precategory : UU (l1 ⊔ l2) + coalgebra-comonad-Precategory = + Σ ( obj-Precategory C) + ( λ A → + Σ ( hom-Precategory C A (obj-endofunctor-comonad-Precategory C T A)) + ( λ a → is-coalgebra-comonad-Precategory a)) + + obj-coalgebra-comonad-Precategory : + coalgebra-comonad-Precategory → obj-Precategory C + obj-coalgebra-comonad-Precategory = pr1 + + hom-coalgebra-comonad-Precategory : + (f : coalgebra-comonad-Precategory) → + hom-Precategory C + ( obj-coalgebra-comonad-Precategory f) + ( obj-endofunctor-comonad-Precategory C T + ( obj-coalgebra-comonad-Precategory f)) + hom-coalgebra-comonad-Precategory f = pr1 (pr2 f) + + comm-coalgebra-comonad-Precategory : + (f : coalgebra-comonad-Precategory) → + is-coalgebra-comonad-Precategory (hom-coalgebra-comonad-Precategory f) + comm-coalgebra-comonad-Precategory f = pr2 (pr2 f) + + counit-law-coalgebra-comonad-Precategory : + (f : coalgebra-comonad-Precategory) → + has-counit-law-coalgebra-comonad-Precategory + ( hom-coalgebra-comonad-Precategory f) + counit-law-coalgebra-comonad-Precategory f = pr1 (pr2 (pr2 f)) + + comul-law-coalgebra-comonad-Precategory : + (f : coalgebra-comonad-Precategory) → + has-comul-law-coalgebra-comonad-Precategory + ( hom-coalgebra-comonad-Precategory f) + comul-law-coalgebra-comonad-Precategory f = pr2 (pr2 (pr2 f)) +``` diff --git a/src/category-theory/comonads-on-precategories.lagda.md b/src/category-theory/comonads-on-precategories.lagda.md new file mode 100644 index 0000000000..24b39bc238 --- /dev/null +++ b/src/category-theory/comonads-on-precategories.lagda.md @@ -0,0 +1,448 @@ +# Comonads on precategories + +```agda +module category-theory.comonads-on-precategories where +``` + +
Imports + +```agda +open import category-theory.adjunctions-precategories +open import category-theory.commuting-squares-of-morphisms-in-precategories +open import category-theory.copointed-endofunctors-precategories +open import category-theory.functors-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.natural-transformations-maps-precategories +open import category-theory.precategories + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equality-cartesian-product-types +open import foundation.identity-types +open import foundation.sets +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.commuting-squares-of-maps +open import foundation-core.equality-dependent-pair-types +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.propositions +open import foundation-core.transport-along-identifications +``` + +
+ +## Idea + +A +{{#concept "comonad" Disambiguation="on a precategory" Agda=comonad-Precategory}} +on a [precategory](category-theory.precategories.md) `C` consists of an +[endofunctor](category-theory.functors-precategories.md) `T : C → C` together +with two +[natural transformations](category-theory.natural-transformations-functors-precategories.md): +`ε : T ⇒ 1_C` and `δ : T ⇒ T²`, where `1_C : C → C` is the identity functor for +`C`, and `T²` is the functor `T ∘ T : C → C`. These must satisfy the following +{{#concept "comonad laws" Disambiguation="comonad on a precategory"}}: + +- **Associativity:** `(T • δ) ∘ δ = (δ • T) ∘ δ` +- The **left counit law:** `(T • ε) ∘ δ = 1_T` +- The **right counit law:** `(ε • T) ∘ δ = 1_T`. + +Here, `•` denotes +[whiskering](category-theory.natural-transformations-functors-precategories.md#whiskering), +and `1_T : T ⇒ T` denotes the identity natural transformation for `T`. + +See also the dual notion of a +[monad on a precategory](category-theory.monads-on-precategories.md). + +## Definitions + +### Comultiplication structure on a copointed endofunctor on a precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : copointed-endofunctor-Precategory C) + where + + structure-comultiplication-copointed-endofunctor-Precategory : UU (l1 ⊔ l2) + structure-comultiplication-copointed-endofunctor-Precategory = + natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) +``` + +### Associativity of comultiplication on a copointed endofunctor on a precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : copointed-endofunctor-Precategory C) + (μ : structure-comultiplication-copointed-endofunctor-Precategory C T) + where + + associative-comul-copointed-endofunctor-Precategory : UU (l1 ⊔ l2) + associative-comul-copointed-endofunctor-Precategory = + comp-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T))) + ( left-whisker-natural-transformation-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( functor-copointed-endofunctor-Precategory C T) + ( μ)) + ( μ) ＝ + comp-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T))) + ( right-whisker-natural-transformation-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) + + associative-comul-hom-family-copointed-endofunctor-Precategory : UU (l1 ⊔ l2) + associative-comul-hom-family-copointed-endofunctor-Precategory = + ( λ x → + ( comp-hom-Precategory C + ( hom-functor-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) + ( x))) + ( hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) + ( x)))) ~ + ( λ x → + ( comp-hom-Precategory C + ( hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) + ( obj-functor-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( x))) + ( hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) + ( x)))) +``` + +### The left counit law on a comultiplication on a copointed endofunctor + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : copointed-endofunctor-Precategory C) + (μ : structure-comultiplication-copointed-endofunctor-Precategory C T) + where + + left-counit-law-comul-copointed-endofunctor-Precategory : UU (l1 ⊔ l2) + left-counit-law-comul-copointed-endofunctor-Precategory = + comp-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( functor-copointed-endofunctor-Precategory C T) + ( left-whisker-natural-transformation-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( id-functor-Precategory C) + ( functor-copointed-endofunctor-Precategory C T) + ( copointing-copointed-endofunctor-Precategory C T)) + ( μ) ＝ + id-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + + left-counit-law-comul-hom-family-copointed-endofunctor-Precategory : + UU (l1 ⊔ l2) + left-counit-law-comul-hom-family-copointed-endofunctor-Precategory = + ( λ x → + comp-hom-Precategory C + ( hom-functor-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( id-functor-Precategory C) + ( copointing-copointed-endofunctor-Precategory C T) + ( x))) + ( hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) + ( x))) ~ + ( λ x → id-hom-Precategory C) +``` + +### The right counit law on a comultiplication on a copointed endofunctor + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : copointed-endofunctor-Precategory C) + (μ : structure-comultiplication-copointed-endofunctor-Precategory C T) + where + + right-counit-law-comul-copointed-endofunctor-Precategory : UU (l1 ⊔ l2) + right-counit-law-comul-copointed-endofunctor-Precategory = + comp-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( functor-copointed-endofunctor-Precategory C T) + ( right-whisker-natural-transformation-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( id-functor-Precategory C) + ( copointing-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) ＝ + id-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + + right-counit-law-comul-hom-family-copointed-endofunctor-Precategory : + UU (l1 ⊔ l2) + right-counit-law-comul-hom-family-copointed-endofunctor-Precategory = + ( λ x → + comp-hom-Precategory C + ( hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( id-functor-Precategory C) + ( copointing-copointed-endofunctor-Precategory C T) + ( obj-functor-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) x)) + ( hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory C T) + ( comp-functor-Precategory C C C + ( functor-copointed-endofunctor-Precategory C T) + ( functor-copointed-endofunctor-Precategory C T)) + ( μ) + ( x))) ~ + ( λ x → id-hom-Precategory C) +``` + +### The structure of a comonad on a copointed endofunctor on a precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : copointed-endofunctor-Precategory C) + where + + structure-comonad-copointed-endofunctor-Precategory : UU (l1 ⊔ l2) + structure-comonad-copointed-endofunctor-Precategory = + Σ ( structure-comultiplication-copointed-endofunctor-Precategory C T) + ( λ μ → + associative-comul-copointed-endofunctor-Precategory C T μ × + left-counit-law-comul-copointed-endofunctor-Precategory C T μ × + right-counit-law-comul-copointed-endofunctor-Precategory C T μ) +``` + +### The type of comonads on precategories + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + comonad-Precategory : UU (l1 ⊔ l2) + comonad-Precategory = + Σ ( copointed-endofunctor-Precategory C) + ( structure-comonad-copointed-endofunctor-Precategory C) + + module _ + (T : comonad-Precategory) + where + + copointed-endofunctor-comonad-Precategory : + copointed-endofunctor-Precategory C + copointed-endofunctor-comonad-Precategory = pr1 T + + endofunctor-comonad-Precategory : + functor-Precategory C C + endofunctor-comonad-Precategory = + functor-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + + obj-endofunctor-comonad-Precategory : + obj-Precategory C → obj-Precategory C + obj-endofunctor-comonad-Precategory = + obj-functor-Precategory C C endofunctor-comonad-Precategory + + hom-endofunctor-comonad-Precategory : + {X Y : obj-Precategory C} → + hom-Precategory C X Y → + hom-Precategory C + ( obj-endofunctor-comonad-Precategory X) + ( obj-endofunctor-comonad-Precategory Y) + hom-endofunctor-comonad-Precategory = + hom-functor-Precategory C C endofunctor-comonad-Precategory + + preserves-id-endofunctor-comonad-Precategory : + (X : obj-Precategory C) → + hom-endofunctor-comonad-Precategory (id-hom-Precategory C {X}) ＝ + id-hom-Precategory C + preserves-id-endofunctor-comonad-Precategory = + preserves-id-functor-Precategory C C endofunctor-comonad-Precategory + + preserves-comp-endofunctor-comonad-Precategory : + {X Y Z : obj-Precategory C} → + (g : hom-Precategory C Y Z) (f : hom-Precategory C X Y) → + hom-endofunctor-comonad-Precategory (comp-hom-Precategory C g f) ＝ + comp-hom-Precategory C + ( hom-endofunctor-comonad-Precategory g) + ( hom-endofunctor-comonad-Precategory f) + preserves-comp-endofunctor-comonad-Precategory = + preserves-comp-functor-Precategory C C + ( endofunctor-comonad-Precategory) + + counit-comonad-Precategory : + copointing-endofunctor-Precategory C endofunctor-comonad-Precategory + counit-comonad-Precategory = + copointing-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + + hom-counit-comonad-Precategory : + hom-family-functor-Precategory C C + ( endofunctor-comonad-Precategory) + ( id-functor-Precategory C) + hom-counit-comonad-Precategory = + hom-family-copointing-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + + naturality-counit-comonad-Precategory : + is-natural-transformation-Precategory C C + ( endofunctor-comonad-Precategory) + ( id-functor-Precategory C) + ( hom-counit-comonad-Precategory) + naturality-counit-comonad-Precategory = + naturality-copointing-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + + comul-comonad-Precategory : + structure-comultiplication-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + comul-comonad-Precategory = pr1 (pr2 T) + + hom-comul-comonad-Precategory : + hom-family-functor-Precategory C C + ( endofunctor-comonad-Precategory) + ( comp-functor-Precategory C C C + ( endofunctor-comonad-Precategory) + ( endofunctor-comonad-Precategory)) + hom-comul-comonad-Precategory = + hom-family-natural-transformation-Precategory C C + ( endofunctor-comonad-Precategory) + ( comp-functor-Precategory C C C + ( endofunctor-comonad-Precategory) + ( endofunctor-comonad-Precategory)) + ( comul-comonad-Precategory) + + naturality-comul-comonad-Precategory : + is-natural-transformation-Precategory C C + ( endofunctor-comonad-Precategory) + ( comp-functor-Precategory C C C + ( endofunctor-comonad-Precategory) + ( endofunctor-comonad-Precategory)) + ( hom-comul-comonad-Precategory) + naturality-comul-comonad-Precategory = + naturality-natural-transformation-Precategory C C + ( endofunctor-comonad-Precategory) + ( comp-functor-Precategory C C C + ( endofunctor-comonad-Precategory) + ( endofunctor-comonad-Precategory)) + ( comul-comonad-Precategory) + + associative-comul-comonad-Precategory : + associative-comul-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + ( comul-comonad-Precategory) + associative-comul-comonad-Precategory = + pr1 (pr2 (pr2 T)) + + associative-comul-hom-family-comonad-Precategory : + associative-comul-hom-family-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + ( comul-comonad-Precategory) + associative-comul-hom-family-comonad-Precategory = + htpy-eq-hom-family-natural-transformation-Precategory C C + ( endofunctor-comonad-Precategory) + ( comp-functor-Precategory C C C + ( endofunctor-comonad-Precategory) + ( comp-functor-Precategory C C C + ( endofunctor-comonad-Precategory) + ( endofunctor-comonad-Precategory))) + ( associative-comul-comonad-Precategory) + + left-counit-law-comul-comonad-Precategory : + left-counit-law-comul-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + ( comul-comonad-Precategory) + left-counit-law-comul-comonad-Precategory = + pr1 (pr2 (pr2 (pr2 T))) + + left-counit-law-comul-hom-family-comonad-Precategory : + left-counit-law-comul-hom-family-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + ( comul-comonad-Precategory) + left-counit-law-comul-hom-family-comonad-Precategory = + htpy-eq-hom-family-natural-transformation-Precategory C C + ( endofunctor-comonad-Precategory) + ( endofunctor-comonad-Precategory) + ( left-counit-law-comul-comonad-Precategory) + + right-counit-law-comul-comonad-Precategory : + right-counit-law-comul-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + ( comul-comonad-Precategory) + right-counit-law-comul-comonad-Precategory = + pr2 (pr2 (pr2 (pr2 T))) + + right-counit-law-comul-hom-family-comonad-Precategory : + right-counit-law-comul-hom-family-copointed-endofunctor-Precategory C + ( copointed-endofunctor-comonad-Precategory) + ( comul-comonad-Precategory) + right-counit-law-comul-hom-family-comonad-Precategory = + htpy-eq-hom-family-natural-transformation-Precategory C C + ( endofunctor-comonad-Precategory) + ( endofunctor-comonad-Precategory) + ( right-counit-law-comul-comonad-Precategory) +``` diff --git a/src/category-theory/copointed-endofunctors-precategories.lagda.md b/src/category-theory/copointed-endofunctors-precategories.lagda.md new file mode 100644 index 0000000000..478d61045e --- /dev/null +++ b/src/category-theory/copointed-endofunctors-precategories.lagda.md @@ -0,0 +1,142 @@ +# Copointed endofunctors + +```agda +module category-theory.copointed-endofunctors-precategories where +``` + +
Imports + +```agda +open import category-theory.functors-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.precategories + +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +An [endofunctor](category-theory.functors-precategories.md) `F : C → C` on a +[precategory](category-theory.precategories.md) `C` is said to be +{{#concept "copointed" Disambiguation="endofunctor on a category" Agda=copointed-endofunctor-Precategory}} +if it comes equipped with a +[natural transformation](category-theory.natural-transformations-functors-precategories.md) +`id ⇒ F` from the identity [functor](category-theory.functors-precategories.md) +to `F`. + +More explicitly, a +{{#concept "copointing" Disambiguation="endofunctor on a precategory" Agda=copointing-endofunctor-Precategory}} +of an endofunctor `F : C → C` consists of a family of morphisms `ε X : F X → X` +such that for each morphism `f : X → Y` in `C` the diagram + +```text + ε X + F X -----> X + | | + F f | | f + ∨ ∨ + F Y -----> Y + ε Y +``` + +[commutes](category-theory.commuting-squares-of-morphisms-in-precategories.md). + +## Definitions + +### The structure of a copointing on an endofunctor on a precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) (T : functor-Precategory C C) + where + + copointing-endofunctor-Precategory : UU (l1 ⊔ l2) + copointing-endofunctor-Precategory = + natural-transformation-Precategory C C T (id-functor-Precategory C) +``` + +### Copointed endofunctors on a precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + copointed-endofunctor-Precategory : UU (l1 ⊔ l2) + copointed-endofunctor-Precategory = + Σ (functor-Precategory C C) (copointing-endofunctor-Precategory C) + + module _ + (F : copointed-endofunctor-Precategory) + where + + functor-copointed-endofunctor-Precategory : + functor-Precategory C C + functor-copointed-endofunctor-Precategory = + pr1 F + + obj-copointed-endofunctor-Precategory : + obj-Precategory C → obj-Precategory C + obj-copointed-endofunctor-Precategory = + obj-functor-Precategory C C functor-copointed-endofunctor-Precategory + + hom-copointed-endofunctor-Precategory : + {X Y : obj-Precategory C} → + hom-Precategory C X Y → + hom-Precategory C + ( obj-copointed-endofunctor-Precategory X) + ( obj-copointed-endofunctor-Precategory Y) + hom-copointed-endofunctor-Precategory = + hom-functor-Precategory C C functor-copointed-endofunctor-Precategory + + preserves-id-copointed-endofunctor-Precategory : + (X : obj-Precategory C) → + hom-copointed-endofunctor-Precategory (id-hom-Precategory C {X}) ＝ + id-hom-Precategory C + preserves-id-copointed-endofunctor-Precategory = + preserves-id-functor-Precategory C C + ( functor-copointed-endofunctor-Precategory) + + preserves-comp-copointed-endofunctor-Precategory : + {X Y Z : obj-Precategory C} + (g : hom-Precategory C Y Z) (f : hom-Precategory C X Y) → + hom-copointed-endofunctor-Precategory + ( comp-hom-Precategory C g f) ＝ + comp-hom-Precategory C + ( hom-copointed-endofunctor-Precategory g) + ( hom-copointed-endofunctor-Precategory f) + preserves-comp-copointed-endofunctor-Precategory = + preserves-comp-functor-Precategory C C + ( functor-copointed-endofunctor-Precategory) + + copointing-copointed-endofunctor-Precategory : + natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory) + ( id-functor-Precategory C) + copointing-copointed-endofunctor-Precategory = pr2 F + + hom-family-copointing-copointed-endofunctor-Precategory : + hom-family-functor-Precategory C C + ( functor-copointed-endofunctor-Precategory) + ( id-functor-Precategory C) + hom-family-copointing-copointed-endofunctor-Precategory = + hom-family-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory) + ( id-functor-Precategory C) + ( copointing-copointed-endofunctor-Precategory) + + naturality-copointing-copointed-endofunctor-Precategory : + is-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory) + ( id-functor-Precategory C) + ( hom-family-copointing-copointed-endofunctor-Precategory) + naturality-copointing-copointed-endofunctor-Precategory = + naturality-natural-transformation-Precategory C C + ( functor-copointed-endofunctor-Precategory) + ( id-functor-Precategory C) + ( copointing-copointed-endofunctor-Precategory) +``` diff --git a/src/category-theory/monads-on-precategories.lagda.md b/src/category-theory/monads-on-precategories.lagda.md index 2cdc8894f6..0ef7100406 100644 --- a/src/category-theory/monads-on-precategories.lagda.md +++ b/src/category-theory/monads-on-precategories.lagda.md @@ -116,9 +116,9 @@ module _ ( comp-functor-Precategory C C C ( functor-pointed-endofunctor-Precategory C T) ( functor-pointed-endofunctor-Precategory C T)) - ( functor-pointed-endofunctor-Precategory C T) - ( μ) - ( functor-pointed-endofunctor-Precategory C T)) + ( functor-pointed-endofunctor-Precategory C T) + ( μ) + ( functor-pointed-endofunctor-Precategory C T)) associative-mul-hom-family-pointed-endofunctor-Precategory : UU (l1 ⊔ l2) associative-mul-hom-family-pointed-endofunctor-Precategory = diff --git a/src/category-theory/morphisms-coalgebras-comonads-on-precategories.lagda.md b/src/category-theory/morphisms-coalgebras-comonads-on-precategories.lagda.md new file mode 100644 index 0000000000..5b8586a57f --- /dev/null +++ b/src/category-theory/morphisms-coalgebras-comonads-on-precategories.lagda.md @@ -0,0 +1,121 @@ +# Morphisms of coalgebras over comonads on precategories + +```agda +module category-theory.morphisms-coalgebras-comonads-on-precategories where +``` + +
Imports + +```agda +open import category-theory.coalgebras-comonads-on-precategories +open import category-theory.commuting-squares-of-morphisms-in-precategories +open import category-theory.comonads-on-precategories +open import category-theory.precategories + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.sets +open import foundation.universe-levels +``` + +
+ +## Idea + +A +{{#concept "morphism" Disambiguation="of comonad coalgebras on a precategory" Agda=coalgebra-comonad-Precategory}} +between +[comonad coalgebras](category-theory.coalgebras-comonads-on-precategories.md) +`a : A → TA` and `b : B → TB` is a map `f : A → B` such that `Tf ∘ b = a ∘ f`. + +## Definitions + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : comonad-Precategory C) + where + + coherence-morphism-coalgebra-comonad-Precategory : + (f g : coalgebra-comonad-Precategory C T) → + hom-Precategory C + ( obj-coalgebra-comonad-Precategory C T f) + ( obj-coalgebra-comonad-Precategory C T g) → + UU l2 + coherence-morphism-coalgebra-comonad-Precategory f g h = + coherence-square-hom-Precategory C + ( h) + ( hom-coalgebra-comonad-Precategory C T f) + ( hom-coalgebra-comonad-Precategory C T g) + ( hom-endofunctor-comonad-Precategory C T h) + + morphism-coalgebra-comonad-Precategory : + (f g : coalgebra-comonad-Precategory C T) → UU l2 + morphism-coalgebra-comonad-Precategory f g = + Σ ( hom-Precategory C + ( obj-coalgebra-comonad-Precategory C T f) + ( obj-coalgebra-comonad-Precategory C T g)) + ( coherence-morphism-coalgebra-comonad-Precategory f g) + + hom-morphism-coalgebra-comonad-Precategory : + (f g : coalgebra-comonad-Precategory C T) + (h : morphism-coalgebra-comonad-Precategory f g) → + hom-Precategory C + ( obj-coalgebra-comonad-Precategory C T f) + ( obj-coalgebra-comonad-Precategory C T g) + hom-morphism-coalgebra-comonad-Precategory f g h = pr1 h + + bottom-hom-morphism-coalgebra-comonad-Precategory : + (f g : coalgebra-comonad-Precategory C T) + (h : morphism-coalgebra-comonad-Precategory f g) → + hom-Precategory C + ( obj-endofunctor-comonad-Precategory C T + ( obj-coalgebra-comonad-Precategory C T f)) + ( obj-endofunctor-comonad-Precategory C T + ( obj-coalgebra-comonad-Precategory C T g)) + bottom-hom-morphism-coalgebra-comonad-Precategory f g h = + hom-endofunctor-comonad-Precategory C T + ( hom-morphism-coalgebra-comonad-Precategory f g h) + + comm-hom-morphism-coalgebra-comonad-Precategory : + (f g : coalgebra-comonad-Precategory C T) + (h : morphism-coalgebra-comonad-Precategory f g) → + coherence-square-hom-Precategory C + ( hom-morphism-coalgebra-comonad-Precategory f g h) + ( hom-coalgebra-comonad-Precategory C T f) + ( hom-coalgebra-comonad-Precategory C T g) + ( bottom-hom-morphism-coalgebra-comonad-Precategory f g h) + comm-hom-morphism-coalgebra-comonad-Precategory f g h = pr2 h + + comp-morphism-coalgebra-comonad-Precategory : + (a b c : coalgebra-comonad-Precategory C T) + (g : morphism-coalgebra-comonad-Precategory b c) → + (f : morphism-coalgebra-comonad-Precategory a b) → + morphism-coalgebra-comonad-Precategory a c + comp-morphism-coalgebra-comonad-Precategory a b c g f = + ( comp-hom-Precategory C + ( hom-morphism-coalgebra-comonad-Precategory b c g) + ( hom-morphism-coalgebra-comonad-Precategory a b f)) , + (ap + (precomp-hom-Precategory C (hom-coalgebra-comonad-Precategory C T a) _) + (preserves-comp-endofunctor-comonad-Precategory C T _ _)) ∙ + ( pasting-horizontal-coherence-square-hom-Precategory C + ( hom-morphism-coalgebra-comonad-Precategory a b f) + ( hom-morphism-coalgebra-comonad-Precategory b c g) + ( hom-coalgebra-comonad-Precategory C T a) + ( hom-coalgebra-comonad-Precategory C T b) + ( hom-coalgebra-comonad-Precategory C T c) + ( bottom-hom-morphism-coalgebra-comonad-Precategory a b f) + ( bottom-hom-morphism-coalgebra-comonad-Precategory b c g) + ( comm-hom-morphism-coalgebra-comonad-Precategory a b f) + ( comm-hom-morphism-coalgebra-comonad-Precategory b c g)) + + is-set-morphism-coalgebra-comonad-Precategory : + (f g : coalgebra-comonad-Precategory C T) → + is-set (morphism-coalgebra-comonad-Precategory f g) + is-set-morphism-coalgebra-comonad-Precategory f g = + is-set-Σ + ( is-set-hom-Precategory C _ _) + ( λ hk → is-set-is-prop (is-set-hom-Precategory C _ _ _ _)) +``` diff --git a/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md b/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md new file mode 100644 index 0000000000..91466df096 --- /dev/null +++ b/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md @@ -0,0 +1,357 @@ +# The precategory of coalgebras of a comonad + +```agda +module category-theory.precategory-of-coalgebras-comonads-on-precategories where +``` + +
Imports + +```agda +open import category-theory.adjunctions-precategories +open import category-theory.coalgebras-comonads-on-precategories +open import category-theory.comonads-on-precategories +open import category-theory.functors-precategories +open import category-theory.morphisms-coalgebras-comonads-on-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.precategories + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.sets +open import foundation.universe-levels + +open import foundation-core.cartesian-product-types +open import foundation-core.equality-dependent-pair-types +open import foundation-core.equivalences +open import foundation-core.function-types +open import foundation-core.homotopies +open import foundation-core.propositions +open import foundation-core.transport-along-identifications +``` + +
+ +## Idea + +The +{{#concept "precategory of coalgebras" Disambiguation="of a comonad on a precategory" Agda=coalgebras-comonad-Precategory}} +of a [comonad on a precategory](category-theory.comonads-on-precategories.md) +`T`, denoted `EM(T)`, also called the **Eilenberg–Moore precategory**, consists +of all `T`-coalgebras and `T`-coalgebra morphisms. It comes with an adjunction +`EM(T) ⇄ C`. + +## Definitions + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : comonad-Precategory C) + where + + obj-coalgebras-comonad-Precategory : + UU (l1 ⊔ l2) + obj-coalgebras-comonad-Precategory = coalgebra-comonad-Precategory C T + + hom-set-coalgebras-comonad-Precategory : + (a b : obj-coalgebras-comonad-Precategory) → + Set l2 + hom-set-coalgebras-comonad-Precategory a b = + ( morphism-coalgebra-comonad-Precategory C T a b) , + ( is-set-morphism-coalgebra-comonad-Precategory C T a b) + + hom-coalgebras-comonad-Precategory : + (a b : obj-coalgebras-comonad-Precategory) → + UU l2 + hom-coalgebras-comonad-Precategory a b = + type-Set (hom-set-coalgebras-comonad-Precategory a b) + + comp-hom-coalgebras-comonad-Precategory : + (a b c : obj-coalgebras-comonad-Precategory) + (g : hom-coalgebras-comonad-Precategory b c) + (f : hom-coalgebras-comonad-Precategory a b) → + hom-coalgebras-comonad-Precategory a c + comp-hom-coalgebras-comonad-Precategory a b c g f = + comp-morphism-coalgebra-comonad-Precategory C T a b c g f + + coh-id-hom-coalgebras-comonad-Precategory : + (x : obj-coalgebras-comonad-Precategory) → + coherence-morphism-coalgebra-comonad-Precategory C T x x + ( id-hom-Precategory C) + coh-id-hom-coalgebras-comonad-Precategory x = + ( ap + ( precomp-hom-Precategory C _ _) + ( preserves-id-endofunctor-comonad-Precategory C T _)) ∙ + ( left-unit-law-comp-hom-Precategory C _) ∙ + ( inv + ( right-unit-law-comp-hom-Precategory C _)) + + id-hom-coalgebras-comonad-Precategory : + (x : obj-coalgebras-comonad-Precategory) → + hom-coalgebras-comonad-Precategory x x + id-hom-coalgebras-comonad-Precategory x = + ( id-hom-Precategory C , coh-id-hom-coalgebras-comonad-Precategory x) + + associative-comp-hom-coalgebras-comonad-Precategory : + (x y z w : obj-coalgebras-comonad-Precategory) + (h : hom-coalgebras-comonad-Precategory z w) + (g : hom-coalgebras-comonad-Precategory y z) + (f : hom-coalgebras-comonad-Precategory x y) → + ( comp-hom-coalgebras-comonad-Precategory x y w + ( comp-hom-coalgebras-comonad-Precategory y z w h g) + ( f)) ＝ + ( comp-hom-coalgebras-comonad-Precategory x z w + ( h) + ( comp-hom-coalgebras-comonad-Precategory x y z g f)) + associative-comp-hom-coalgebras-comonad-Precategory x y z w h g f = + eq-pair-Σ + ( associative-comp-hom-Precategory C _ _ _) + ( eq-is-prop (is-set-hom-Precategory C _ _ _ _)) + + left-counit-law-comp-hom-coalgebras-comonad-Precategory : + (a b : obj-coalgebras-comonad-Precategory) + (f : hom-coalgebras-comonad-Precategory a b) → + ( comp-hom-coalgebras-comonad-Precategory a b b + ( id-hom-coalgebras-comonad-Precategory b) + ( f)) ＝ + ( f) + left-counit-law-comp-hom-coalgebras-comonad-Precategory a b f = + eq-pair-Σ + ( left-unit-law-comp-hom-Precategory C + ( hom-morphism-coalgebra-comonad-Precategory C T a b f)) + ( eq-is-prop (is-set-hom-Precategory C _ _ _ _)) + + right-counit-law-comp-hom-coalgebras-comonad-Precategory : + (a b : obj-coalgebras-comonad-Precategory) + (f : hom-coalgebras-comonad-Precategory a b) → + ( comp-hom-coalgebras-comonad-Precategory a a b + ( f) + ( id-hom-coalgebras-comonad-Precategory a)) ＝ + ( f) + right-counit-law-comp-hom-coalgebras-comonad-Precategory a b f = + eq-pair-Σ + ( right-unit-law-comp-hom-Precategory C + ( hom-morphism-coalgebra-comonad-Precategory C T a b f)) + ( eq-is-prop (is-set-hom-Precategory C _ _ _ _)) + + coalgebras-comonad-Precategory : Precategory (l1 ⊔ l2) l2 + coalgebras-comonad-Precategory = + make-Precategory + ( obj-coalgebras-comonad-Precategory) + ( hom-set-coalgebras-comonad-Precategory) + ( λ {a} {b} {c} g f → comp-hom-coalgebras-comonad-Precategory a b c g f) + ( id-hom-coalgebras-comonad-Precategory) + ( λ {a} {b} {c} {d} h g f → + ( associative-comp-hom-coalgebras-comonad-Precategory a b c d h g f)) + ( λ {a} {b} f → + left-counit-law-comp-hom-coalgebras-comonad-Precategory a b f) + ( λ {a} {b} f → + right-counit-law-comp-hom-coalgebras-comonad-Precategory a b f) +``` + +## Properties + +### Free functor from the underlying category + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : comonad-Precategory C) + (let T₁ = hom-endofunctor-comonad-Precategory C T) + where + + obj-functor-to-coalgebras-comonad-Precategory : + obj-Precategory C → obj-Precategory (coalgebras-comonad-Precategory C T) + obj-functor-to-coalgebras-comonad-Precategory x = + ( obj-endofunctor-comonad-Precategory C T x) , + ( ( hom-comul-comonad-Precategory C T x) , + ( right-counit-law-comul-hom-family-comonad-Precategory C T x) , + ( associative-comul-hom-family-comonad-Precategory C T x)) + + hom-functor-to-coalgebras-comonad-Precategory : + {x y : obj-Precategory C} + (f : hom-Precategory C x y) → + hom-Precategory (coalgebras-comonad-Precategory C T) + ( obj-functor-to-coalgebras-comonad-Precategory x) + ( obj-functor-to-coalgebras-comonad-Precategory y) + hom-functor-to-coalgebras-comonad-Precategory f = + ( T₁ f) , + ( naturality-comul-comonad-Precategory C T f) + + preserves-id-functor-to-coalgebras-comonad-Precategory : + (x : obj-Precategory C) → + hom-functor-to-coalgebras-comonad-Precategory (id-hom-Precategory C {x}) ＝ + id-hom-coalgebras-comonad-Precategory C T + ( obj-functor-to-coalgebras-comonad-Precategory x) + preserves-id-functor-to-coalgebras-comonad-Precategory x = + eq-pair-Σ + ( preserves-id-endofunctor-comonad-Precategory C T x) + ( eq-is-prop (is-set-hom-Precategory C _ _ _ _)) + + preserves-comp-functor-to-coalgebras-comonad-Precategory : + {x y z : obj-Precategory C} → + (g : hom-Precategory C y z) (f : hom-Precategory C x y) → + hom-functor-to-coalgebras-comonad-Precategory (comp-hom-Precategory C g f) ＝ + comp-hom-coalgebras-comonad-Precategory C T + ( obj-functor-to-coalgebras-comonad-Precategory x) + ( obj-functor-to-coalgebras-comonad-Precategory y) + ( obj-functor-to-coalgebras-comonad-Precategory z) + ( hom-functor-to-coalgebras-comonad-Precategory g) + ( hom-functor-to-coalgebras-comonad-Precategory f) + preserves-comp-functor-to-coalgebras-comonad-Precategory g f = + eq-pair-Σ + ( preserves-comp-endofunctor-comonad-Precategory C T g f) + ( eq-is-prop (is-set-hom-Precategory C _ _ _ _)) + + functor-to-coalgebras-comonad-Precategory : + functor-Precategory C (coalgebras-comonad-Precategory C T) + functor-to-coalgebras-comonad-Precategory = + ( obj-functor-to-coalgebras-comonad-Precategory) , + ( hom-functor-to-coalgebras-comonad-Precategory) , + ( preserves-comp-functor-to-coalgebras-comonad-Precategory) , + ( preserves-id-functor-to-coalgebras-comonad-Precategory) +``` + +### Forgetful functor from the underlying precategory + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : comonad-Precategory C) + where + + obj-functor-from-coalgebras-comonad-Precategory : + obj-coalgebras-comonad-Precategory C T → obj-Precategory C + obj-functor-from-coalgebras-comonad-Precategory = + obj-coalgebra-comonad-Precategory C T + + hom-functor-from-coalgebras-comonad-Precategory : + (x y : obj-coalgebras-comonad-Precategory C T) + (f : hom-coalgebras-comonad-Precategory C T x y) → + hom-Precategory C + ( obj-functor-from-coalgebras-comonad-Precategory x) + ( obj-functor-from-coalgebras-comonad-Precategory y) + hom-functor-from-coalgebras-comonad-Precategory = + hom-morphism-coalgebra-comonad-Precategory C T + + preserves-id-functor-from-coalgebras-comonad-Precategory : + (x : obj-coalgebras-comonad-Precategory C T) → + hom-functor-from-coalgebras-comonad-Precategory x x + ( id-hom-coalgebras-comonad-Precategory C T x) ＝ + id-hom-Precategory C + preserves-id-functor-from-coalgebras-comonad-Precategory x = refl + + preserves-comp-functor-from-coalgebras-comonad-Precategory : + (x y z : obj-coalgebras-comonad-Precategory C T) + (g : hom-coalgebras-comonad-Precategory C T y z) + (f : hom-coalgebras-comonad-Precategory C T x y) → + hom-functor-from-coalgebras-comonad-Precategory x z + ( comp-hom-coalgebras-comonad-Precategory C T x y z g f) ＝ + comp-hom-Precategory C + ( hom-functor-from-coalgebras-comonad-Precategory y z g) + ( hom-functor-from-coalgebras-comonad-Precategory x y f) + preserves-comp-functor-from-coalgebras-comonad-Precategory x y z g f = refl + + functor-from-coalgebras-comonad-Precategory : + functor-Precategory (coalgebras-comonad-Precategory C T) C + functor-from-coalgebras-comonad-Precategory = + ( obj-functor-from-coalgebras-comonad-Precategory) , + ( λ {x} {y} f → hom-functor-from-coalgebras-comonad-Precategory x y f) , + ( λ {x} {y} {z} g f → + preserves-comp-functor-from-coalgebras-comonad-Precategory x y z g f) , + ( preserves-id-functor-from-coalgebras-comonad-Precategory) +``` + +### Adjunction with the underlying category + +The counit of the adjunction between these two functors is exactly the counit of +the comonad. + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : comonad-Precategory C) + where + + counit-coalgebras-comonad-Precategory : + natural-transformation-Precategory C C + ( comp-functor-Precategory C (coalgebras-comonad-Precategory C T) C + ( functor-from-coalgebras-comonad-Precategory C T) + ( functor-to-coalgebras-comonad-Precategory C T)) + ( id-functor-Precategory C) + counit-coalgebras-comonad-Precategory = counit-comonad-Precategory C T +``` + +The unit is the horizontal map given by the structure map of the coalgebra + +```text + a + x -----> Tx + | | + a | | δ + ∨ ∨ + Tx -----> T²x. + Ta +``` + +```agda + unit-coalgebras-comonad-Precategory : + natural-transformation-Precategory + ( coalgebras-comonad-Precategory C T) + ( coalgebras-comonad-Precategory C T) + ( id-functor-Precategory (coalgebras-comonad-Precategory C T)) + ( comp-functor-Precategory + ( coalgebras-comonad-Precategory C T) + ( C) + ( coalgebras-comonad-Precategory C T) + ( functor-to-coalgebras-comonad-Precategory C T) + ( functor-from-coalgebras-comonad-Precategory C T)) + unit-coalgebras-comonad-Precategory = + ( λ x → + ( hom-coalgebra-comonad-Precategory C T x) , + ( comul-law-coalgebra-comonad-Precategory C T x)) , + ( λ {x} {y} f → + eq-pair-Σ + ( comm-hom-morphism-coalgebra-comonad-Precategory C T x y f) + ( eq-is-prop (is-set-hom-Precategory C _ _ _ _))) + + right-triangle-coalgebras-comonad-Precategory : + has-right-triangle-identity-Precategory + ( coalgebras-comonad-Precategory C T) + ( C) + ( functor-from-coalgebras-comonad-Precategory C T) + ( functor-to-coalgebras-comonad-Precategory C T) + ( unit-coalgebras-comonad-Precategory) + ( counit-coalgebras-comonad-Precategory) + right-triangle-coalgebras-comonad-Precategory x = + eq-pair-Σ + ( left-counit-law-comul-hom-family-comonad-Precategory C T x) + ( eq-is-prop (is-set-hom-Precategory C _ _ _ _)) + + left-triangle-coalgebras-comonad-Precategory : + has-left-triangle-identity-Precategory + ( coalgebras-comonad-Precategory C T) + ( C) + ( functor-from-coalgebras-comonad-Precategory C T) + ( functor-to-coalgebras-comonad-Precategory C T) + ( unit-coalgebras-comonad-Precategory) + ( counit-coalgebras-comonad-Precategory) + left-triangle-coalgebras-comonad-Precategory x = + counit-law-coalgebra-comonad-Precategory C T x + + adjunction-coalgebras-comonad-Precategory : + Adjunction-Precategory (coalgebras-comonad-Precategory C T) C + adjunction-coalgebras-comonad-Precategory = + make-Adjunction-Precategory (coalgebras-comonad-Precategory C T) C + ( functor-from-coalgebras-comonad-Precategory C T) + ( functor-to-coalgebras-comonad-Precategory C T) + ( is-adjoint-pair-unit-counit-Precategory + ( coalgebras-comonad-Precategory C T) + ( C) + ( functor-from-coalgebras-comonad-Precategory C T) + ( functor-to-coalgebras-comonad-Precategory C T) + ( unit-coalgebras-comonad-Precategory) + ( counit-coalgebras-comonad-Precategory) + ( left-triangle-coalgebras-comonad-Precategory) + ( right-triangle-coalgebras-comonad-Precategory)) +``` From 08327450f6acad885d8d3e1f21e2d899d7c8927b Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Mon, 9 Jun 2025 13:46:44 -0400 Subject: [PATCH 03/20] Suggested fixes --- .../left-extensions-precategories.lagda.md | 15 ++++++++------- .../left-kan-extensions-precategories.lagda.md | 9 ++++++++- .../right-extensions-precategories.lagda.md | 17 +++++++++-------- .../right-kan-extensions-precategories.lagda.md | 9 ++++++++- 4 files changed, 33 insertions(+), 17 deletions(-) diff --git a/src/category-theory/left-extensions-precategories.lagda.md b/src/category-theory/left-extensions-precategories.lagda.md index 1214b92702..557488579f 100644 --- a/src/category-theory/left-extensions-precategories.lagda.md +++ b/src/category-theory/left-extensions-precategories.lagda.md @@ -52,16 +52,17 @@ of a [functor](category-theory.functors-precategories.md) `F : C → D` between `φ : F → G ∘ p`. ```text - C - | \ - p F - | \ - ∨ ∨ - C' - G -> D + C + | \ + p | \ F + | \ + ∨ ∨ + C' -----> D + G ``` We note that this is not a standard definition, but it inspired by the notion of -a [left kan extension](category-theory.left-kan-extensions-precategories.md). +a [left Kan extension](category-theory.left-kan-extensions-precategories.md). ## Definition diff --git a/src/category-theory/left-kan-extensions-precategories.lagda.md b/src/category-theory/left-kan-extensions-precategories.lagda.md index 9f23b81ffc..5955b56b20 100644 --- a/src/category-theory/left-kan-extensions-precategories.lagda.md +++ b/src/category-theory/left-kan-extensions-precategories.lagda.md @@ -28,11 +28,18 @@ of [functor](category-theory.functors-precategories.md) `F : C → D` between [precategories](category-theory.precategories.md) along another functor `p : C → C'` is the universal [left extension](category-theory.left-extensions-precategories.md) of `F` along -`p`. +`p`. That is, `(L, α)` is a left Kan extension if for every other left extension +`(G, β)` there is a unique natural transformation `γ : L ⇒ G` such that +`γ ∘ α = β`. In particular, `(L, α)` is initial in the category of left +extensions of `F` along `p`. More concretely, we require the function `left-extension-map-Precategory` to be an equivalence. +See also +[right Kan extension](category-theory.right-kan-extensions-precategories.md) for +the dual concept. + ## Definition ```agda diff --git a/src/category-theory/right-extensions-precategories.lagda.md b/src/category-theory/right-extensions-precategories.lagda.md index 4c3828347f..dea6a439ec 100644 --- a/src/category-theory/right-extensions-precategories.lagda.md +++ b/src/category-theory/right-extensions-precategories.lagda.md @@ -52,16 +52,17 @@ of a [functor](category-theory.functors-precategories.md) `F : C → D` between `φ : G ∘ p → F`. ```text - C - | \ - p F - | \ - ∨ ∨ - C' - G -> D + C + | \ + p | \ F + | \ + ∨ ∨ + C' -----> D + G ``` -We note that this is not a standard definition, but it inspired by the notion of -a [right kan extension](category-theory.right-kan-extensions-precategories.md). +We note that this is not a standard definition, but is inspired by the notion of +a [right Kan extension](category-theory.right-kan-extensions-precategories.md). ## Definition diff --git a/src/category-theory/right-kan-extensions-precategories.lagda.md b/src/category-theory/right-kan-extensions-precategories.lagda.md index 1af7fd92a1..faf5ca1373 100644 --- a/src/category-theory/right-kan-extensions-precategories.lagda.md +++ b/src/category-theory/right-kan-extensions-precategories.lagda.md @@ -28,11 +28,18 @@ of [functor](category-theory.functors-precategories.md) `F : C → D` between [precategories](category-theory.precategories.md) along another functor `p : C → C'` is the universal [right extension](category-theory.right-extensions-precategories.md) of `F` -along `p`. +along `p`. That is, `(R, α)` is a right Kan extension if for every other right +extension `(G, β)` there is a unique natural transformation `γ : G ⇒ R` such +that `α ∘ γ = β`. In particular, `(R, α)` is terminal in the category of right +extensions of `F` along `p`. More concretely, we require the function `right-extension-map-Precategory` to be an equivalence. +See also +[left Kan extension](category-theory.left-kan-extensions-precategories.md) for +the dual concept. + ## Definition ```agda From 897c6a4d4a23c716c6842983e3043fbf25b182d7 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 10 Jun 2025 10:21:25 -0400 Subject: [PATCH 04/20] Apply suggestions --- .../algebras-monads-on-precategories.lagda.md | 42 ++++++++++--------- ...lgebras-comonads-on-precategories.lagda.md | 42 ++++++++++--------- .../comonads-on-precategories.lagda.md | 5 +++ ...ointed-endofunctors-precategories.lagda.md | 7 +++- .../left-extensions-precategories.lagda.md | 7 +++- ...left-kan-extensions-precategories.lagda.md | 9 ++-- .../monads-on-precategories.lagda.md | 5 +++ ...ointed-endofunctors-precategories.lagda.md | 7 +++- .../right-extensions-precategories.lagda.md | 5 +++ ...ight-kan-extensions-precategories.lagda.md | 9 ++-- 10 files changed, 87 insertions(+), 51 deletions(-) diff --git a/src/category-theory/algebras-monads-on-precategories.lagda.md b/src/category-theory/algebras-monads-on-precategories.lagda.md index d7e375681b..576bc1e908 100644 --- a/src/category-theory/algebras-monads-on-precategories.lagda.md +++ b/src/category-theory/algebras-monads-on-precategories.lagda.md @@ -41,34 +41,36 @@ object `A` and morphism `a : TA → A` satisfying two compatibility laws: module _ {l1 l2 : Level} (C : Precategory l1 l2) (T : monad-Precategory C) + {A : obj-Precategory C} + (a : hom-Precategory C (obj-endofunctor-monad-Precategory C T A) A) where - module _ - {A : obj-Precategory C} - (a : hom-Precategory C (obj-endofunctor-monad-Precategory C T A) A) - where + has-unit-law-algebra-monad-Precategory : UU l2 + has-unit-law-algebra-monad-Precategory = + comp-hom-Precategory C a (hom-unit-monad-Precategory C T A) ＝ + id-hom-Precategory C - has-unit-law-algebra-monad-Precategory : UU l2 - has-unit-law-algebra-monad-Precategory = - comp-hom-Precategory C a (hom-unit-monad-Precategory C T A) ＝ - id-hom-Precategory C + has-mul-law-algebra-monad-Precategory : UU l2 + has-mul-law-algebra-monad-Precategory = + comp-hom-Precategory C a (hom-endofunctor-monad-Precategory C T a) ＝ + comp-hom-Precategory C a (hom-mul-monad-Precategory C T A) - has-mul-law-algebra-monad-Precategory : UU l2 - has-mul-law-algebra-monad-Precategory = - comp-hom-Precategory C a (hom-endofunctor-monad-Precategory C T a) ＝ - comp-hom-Precategory C a (hom-mul-monad-Precategory C T A) + is-algebra-monad-Precategory : UU l2 + is-algebra-monad-Precategory = + has-unit-law-algebra-monad-Precategory × + has-mul-law-algebra-monad-Precategory - is-algebra-monad-Precategory : UU l2 - is-algebra-monad-Precategory = - has-unit-law-algebra-monad-Precategory × - has-mul-law-algebra-monad-Precategory +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : monad-Precategory C) + where algebra-monad-Precategory : UU (l1 ⊔ l2) algebra-monad-Precategory = Σ ( obj-Precategory C) ( λ A → Σ ( hom-Precategory C (obj-endofunctor-monad-Precategory C T A) A) - ( λ a → is-algebra-monad-Precategory a)) + ( λ a → is-algebra-monad-Precategory C T a)) obj-algebra-monad-Precategory : algebra-monad-Precategory → obj-Precategory C obj-algebra-monad-Precategory = pr1 @@ -82,16 +84,16 @@ module _ comm-algebra-monad-Precategory : (f : algebra-monad-Precategory) → - is-algebra-monad-Precategory (hom-algebra-monad-Precategory f) + is-algebra-monad-Precategory C T (hom-algebra-monad-Precategory f) comm-algebra-monad-Precategory f = pr2 (pr2 f) unit-law-algebra-monad-Precategory : (f : algebra-monad-Precategory) → - has-unit-law-algebra-monad-Precategory (hom-algebra-monad-Precategory f) + has-unit-law-algebra-monad-Precategory C T (hom-algebra-monad-Precategory f) unit-law-algebra-monad-Precategory f = pr1 (pr2 (pr2 f)) mul-law-algebra-monad-Precategory : (f : algebra-monad-Precategory) → - has-mul-law-algebra-monad-Precategory (hom-algebra-monad-Precategory f) + has-mul-law-algebra-monad-Precategory C T (hom-algebra-monad-Precategory f) mul-law-algebra-monad-Precategory f = pr2 (pr2 (pr2 f)) ``` diff --git a/src/category-theory/coalgebras-comonads-on-precategories.lagda.md b/src/category-theory/coalgebras-comonads-on-precategories.lagda.md index 663ac55d77..a17d025399 100644 --- a/src/category-theory/coalgebras-comonads-on-precategories.lagda.md +++ b/src/category-theory/coalgebras-comonads-on-precategories.lagda.md @@ -41,34 +41,36 @@ an object `A` and morphism `a : A → TA` satisfying two compatibility laws: module _ {l1 l2 : Level} (C : Precategory l1 l2) (T : comonad-Precategory C) + {A : obj-Precategory C} + (a : hom-Precategory C A (obj-endofunctor-comonad-Precategory C T A)) where - module _ - {A : obj-Precategory C} - (a : hom-Precategory C A (obj-endofunctor-comonad-Precategory C T A)) - where + has-counit-law-coalgebra-comonad-Precategory : UU l2 + has-counit-law-coalgebra-comonad-Precategory = + comp-hom-Precategory C (hom-counit-comonad-Precategory C T A) a ＝ + id-hom-Precategory C - has-counit-law-coalgebra-comonad-Precategory : UU l2 - has-counit-law-coalgebra-comonad-Precategory = - comp-hom-Precategory C (hom-counit-comonad-Precategory C T A) a ＝ - id-hom-Precategory C + has-comul-law-coalgebra-comonad-Precategory : UU l2 + has-comul-law-coalgebra-comonad-Precategory = + comp-hom-Precategory C (hom-endofunctor-comonad-Precategory C T a) a ＝ + comp-hom-Precategory C (hom-comul-comonad-Precategory C T A) a - has-comul-law-coalgebra-comonad-Precategory : UU l2 - has-comul-law-coalgebra-comonad-Precategory = - comp-hom-Precategory C (hom-endofunctor-comonad-Precategory C T a) a ＝ - comp-hom-Precategory C (hom-comul-comonad-Precategory C T A) a + is-coalgebra-comonad-Precategory : UU l2 + is-coalgebra-comonad-Precategory = + has-counit-law-coalgebra-comonad-Precategory × + has-comul-law-coalgebra-comonad-Precategory - is-coalgebra-comonad-Precategory : UU l2 - is-coalgebra-comonad-Precategory = - has-counit-law-coalgebra-comonad-Precategory × - has-comul-law-coalgebra-comonad-Precategory +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (T : comonad-Precategory C) + where coalgebra-comonad-Precategory : UU (l1 ⊔ l2) coalgebra-comonad-Precategory = Σ ( obj-Precategory C) ( λ A → Σ ( hom-Precategory C A (obj-endofunctor-comonad-Precategory C T A)) - ( λ a → is-coalgebra-comonad-Precategory a)) + ( λ a → is-coalgebra-comonad-Precategory C T a)) obj-coalgebra-comonad-Precategory : coalgebra-comonad-Precategory → obj-Precategory C @@ -84,18 +86,18 @@ module _ comm-coalgebra-comonad-Precategory : (f : coalgebra-comonad-Precategory) → - is-coalgebra-comonad-Precategory (hom-coalgebra-comonad-Precategory f) + is-coalgebra-comonad-Precategory C T (hom-coalgebra-comonad-Precategory f) comm-coalgebra-comonad-Precategory f = pr2 (pr2 f) counit-law-coalgebra-comonad-Precategory : (f : coalgebra-comonad-Precategory) → - has-counit-law-coalgebra-comonad-Precategory + has-counit-law-coalgebra-comonad-Precategory C T ( hom-coalgebra-comonad-Precategory f) counit-law-coalgebra-comonad-Precategory f = pr1 (pr2 (pr2 f)) comul-law-coalgebra-comonad-Precategory : (f : coalgebra-comonad-Precategory) → - has-comul-law-coalgebra-comonad-Precategory + has-comul-law-coalgebra-comonad-Precategory C T ( hom-coalgebra-comonad-Precategory f) comul-law-coalgebra-comonad-Precategory f = pr2 (pr2 (pr2 f)) ``` diff --git a/src/category-theory/comonads-on-precategories.lagda.md b/src/category-theory/comonads-on-precategories.lagda.md index 24b39bc238..70fa64cbd2 100644 --- a/src/category-theory/comonads-on-precategories.lagda.md +++ b/src/category-theory/comonads-on-precategories.lagda.md @@ -446,3 +446,8 @@ module _ ( endofunctor-comonad-Precategory) ( right-counit-law-comul-comonad-Precategory) ``` + +## See also + +- [Monads](category-theory.monads-on-precategories.lagda.md) for the dual + concept. diff --git a/src/category-theory/copointed-endofunctors-precategories.lagda.md b/src/category-theory/copointed-endofunctors-precategories.lagda.md index 478d61045e..da5e6667ff 100644 --- a/src/category-theory/copointed-endofunctors-precategories.lagda.md +++ b/src/category-theory/copointed-endofunctors-precategories.lagda.md @@ -1,4 +1,4 @@ -# Copointed endofunctors +# Copointed endofunctors on precategories ```agda module category-theory.copointed-endofunctors-precategories where @@ -140,3 +140,8 @@ module _ ( id-functor-Precategory C) ( copointing-copointed-endofunctor-Precategory) ``` + +## See also + +- [Pointed endofunctors](category-theory.pointed-endofunctors-precategories.md) + for the dual concept. diff --git a/src/category-theory/left-extensions-precategories.lagda.md b/src/category-theory/left-extensions-precategories.lagda.md index 557488579f..e0273c3451 100644 --- a/src/category-theory/left-extensions-precategories.lagda.md +++ b/src/category-theory/left-extensions-precategories.lagda.md @@ -61,7 +61,7 @@ of a [functor](category-theory.functors-precategories.md) `F : C → D` between G ``` -We note that this is not a standard definition, but it inspired by the notion of +We note that this is not a standard definition, but is inspired by the notion of a [left Kan extension](category-theory.left-kan-extensions-precategories.md). ## Definition @@ -249,3 +249,8 @@ module _ eq-htpy-left-extension-Precategory R S = map-inv-equiv (equiv-htpy-eq-left-extension-Precategory R S) ``` + +## See also + +- [Right extensions](category-theory.right-extensions-precategories.md) for the + dual concept. diff --git a/src/category-theory/left-kan-extensions-precategories.lagda.md b/src/category-theory/left-kan-extensions-precategories.lagda.md index 5955b56b20..70404cd987 100644 --- a/src/category-theory/left-kan-extensions-precategories.lagda.md +++ b/src/category-theory/left-kan-extensions-precategories.lagda.md @@ -36,10 +36,6 @@ extensions of `F` along `p`. More concretely, we require the function `left-extension-map-Precategory` to be an equivalence. -See also -[right Kan extension](category-theory.right-kan-extensions-precategories.md) for -the dual concept. - ## Definition ```agda @@ -99,3 +95,8 @@ module _ natural-transformation-left-extension-Precategory C C' D p F left-extension-left-kan-extension-Precategory ``` + +## See also + +- [Right Kan extensions](category-theory.right-kan-extensions-precategories.md) + for the dual concept. diff --git a/src/category-theory/monads-on-precategories.lagda.md b/src/category-theory/monads-on-precategories.lagda.md index 0ef7100406..29bff2fead 100644 --- a/src/category-theory/monads-on-precategories.lagda.md +++ b/src/category-theory/monads-on-precategories.lagda.md @@ -440,3 +440,8 @@ module _ ( endofunctor-monad-Precategory) ( right-unit-law-mul-monad-Precategory) ``` + +## See also + +- [Comonads](category-theory.comonads-on-precategories.lagda.md) for the dual + concept. diff --git a/src/category-theory/pointed-endofunctors-precategories.lagda.md b/src/category-theory/pointed-endofunctors-precategories.lagda.md index 2472a4dab6..453b5b4949 100644 --- a/src/category-theory/pointed-endofunctors-precategories.lagda.md +++ b/src/category-theory/pointed-endofunctors-precategories.lagda.md @@ -1,4 +1,4 @@ -# Pointed endofunctors +# Pointed endofunctors on precategories ```agda module category-theory.pointed-endofunctors-precategories where @@ -139,3 +139,8 @@ module _ ( functor-pointed-endofunctor-Precategory) ( pointing-pointed-endofunctor-Precategory) ``` + +## See also + +- [Coointed endofunctors](category-theory.copointed-endofunctors-precategories.md) + for the dual concept. diff --git a/src/category-theory/right-extensions-precategories.lagda.md b/src/category-theory/right-extensions-precategories.lagda.md index dea6a439ec..cc2b294a35 100644 --- a/src/category-theory/right-extensions-precategories.lagda.md +++ b/src/category-theory/right-extensions-precategories.lagda.md @@ -249,3 +249,8 @@ module _ eq-htpy-right-extension-Precategory R S = map-inv-equiv (equiv-htpy-eq-right-extension-Precategory R S) ``` + +## See also + +- [Left extensions](category-theory.left-extensions-precategories.md) for the + dual concept. diff --git a/src/category-theory/right-kan-extensions-precategories.lagda.md b/src/category-theory/right-kan-extensions-precategories.lagda.md index faf5ca1373..3d9e407cd3 100644 --- a/src/category-theory/right-kan-extensions-precategories.lagda.md +++ b/src/category-theory/right-kan-extensions-precategories.lagda.md @@ -36,10 +36,6 @@ extensions of `F` along `p`. More concretely, we require the function `right-extension-map-Precategory` to be an equivalence. -See also -[left Kan extension](category-theory.left-kan-extensions-precategories.md) for -the dual concept. - ## Definition ```agda @@ -99,3 +95,8 @@ module _ natural-transformation-right-extension-Precategory C C' D p F right-extension-right-kan-extension-Precategory ``` + +## See also + +- [Left Kan extensions](category-theory.left-kan-extensions-precategories.md) + for the dual concept. From b6a4dc014a6031864d9100939a3bee24cb1a305c Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 10 Jun 2025 10:24:47 -0400 Subject: [PATCH 05/20] Remove set-indexed coproducts --- .../coproducts-in-precategories.lagda.md | 36 ------------------- 1 file changed, 36 deletions(-) diff --git a/src/category-theory/coproducts-in-precategories.lagda.md b/src/category-theory/coproducts-in-precategories.lagda.md index bb682ae009..cc72f57907 100644 --- a/src/category-theory/coproducts-in-precategories.lagda.md +++ b/src/category-theory/coproducts-in-precategories.lagda.md @@ -16,7 +16,6 @@ open import foundation.dependent-pair-types open import foundation.identity-types open import foundation.iterated-dependent-product-types open import foundation.propositions -open import foundation.sets open import foundation.uniqueness-quantification open import foundation.universe-levels ``` @@ -157,38 +156,3 @@ module _ (comp-hom-Precategory C (inl-coproduct-obj-Precategory C t y₁ y₂) f) (comp-hom-Precategory C (inr-coproduct-obj-Precategory C t y₁ y₂) g) ``` - -```agda -module _ - {l1 l2 : Level} (C : Precategory l1 l2) - where - - is-coproduct-set-obj-Precategory : - {l : Level} (S : Set l) - (I : type-Set S → obj-Precategory C) → - (c : obj-Precategory C) - (ι : (i : type-Set S) → hom-Precategory C (I i) c) → - UU (l1 ⊔ l2 ⊔ l) - is-coproduct-set-obj-Precategory S I c ι = - (z : obj-Precategory C) → - (f : (i : type-Set S) → hom-Precategory C (I i) z) → - ( uniquely-exists-structure - ( hom-Precategory C c z) - ( λ h → - (i : type-Set S) → - ( comp-hom-Precategory C h (ι i)) ＝ f i)) - - coproduct-set-obj-Precategory : - {l : Level} (S : Set l) - (I : type-Set S → obj-Precategory C) → - UU (l1 ⊔ l2 ⊔ l) - coproduct-set-obj-Precategory S I = - Σ (obj-Precategory C) λ c → - Σ ((i : type-Set S) → hom-Precategory C (I i) c) λ ι → - is-coproduct-set-obj-Precategory S I c ι - - has-all-coproducts-Precategory : (l : Level) → UU (l1 ⊔ l2 ⊔ lsuc l) - has-all-coproducts-Precategory l = - (S : Set l) (I : type-Set S → obj-Precategory C) → - coproduct-set-obj-Precategory S I -``` From f3c262962830bb9f3ab903c5919f5d84bbcdffec Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 10 Jun 2025 10:55:20 -0400 Subject: [PATCH 06/20] Dualize pullbacks; fix some links --- .../comonads-on-precategories.lagda.md | 2 +- .../monads-on-precategories.lagda.md | 2 +- .../pullbacks-in-precategories.lagda.md | 17 +- .../pushouts-in-precategories.lagda.md | 171 ++++++++++++++++++ 4 files changed, 184 insertions(+), 8 deletions(-) create mode 100644 src/category-theory/pushouts-in-precategories.lagda.md diff --git a/src/category-theory/comonads-on-precategories.lagda.md b/src/category-theory/comonads-on-precategories.lagda.md index 70fa64cbd2..7fb283b76e 100644 --- a/src/category-theory/comonads-on-precategories.lagda.md +++ b/src/category-theory/comonads-on-precategories.lagda.md @@ -449,5 +449,5 @@ module _ ## See also -- [Monads](category-theory.monads-on-precategories.lagda.md) for the dual +- [Monads](category-theory.monads-on-precategories.md) for the dual concept. diff --git a/src/category-theory/monads-on-precategories.lagda.md b/src/category-theory/monads-on-precategories.lagda.md index 29bff2fead..a51f7da56b 100644 --- a/src/category-theory/monads-on-precategories.lagda.md +++ b/src/category-theory/monads-on-precategories.lagda.md @@ -443,5 +443,5 @@ module _ ## See also -- [Comonads](category-theory.comonads-on-precategories.lagda.md) for the dual +- [Comonads](category-theory.comonads-on-precategories.md) for the dual concept. diff --git a/src/category-theory/pullbacks-in-precategories.lagda.md b/src/category-theory/pullbacks-in-precategories.lagda.md index aaefb61ec6..49b7e958bd 100644 --- a/src/category-theory/pullbacks-in-precategories.lagda.md +++ b/src/category-theory/pullbacks-in-precategories.lagda.md @@ -106,10 +106,10 @@ module _ hom-Precategory C object-pullback-obj-Precategory z pr2-pullback-obj-Precategory = pr1 (pr2 (pr2 (t x y z f g))) - pullback-square-Precategory-comm : + comm-pullback-obj-Precategory : comp-hom-Precategory C f pr1-pullback-obj-Precategory ＝ comp-hom-Precategory C g pr2-pullback-obj-Precategory - pullback-square-Precategory-comm = pr1 (pr2 (pr2 (pr2 (t x y z f g)))) + comm-pullback-obj-Precategory = pr1 (pr2 (pr2 (pr2 (t x y z f g)))) module _ (w' : obj-Precategory C) @@ -123,20 +123,20 @@ module _ morphism-into-pullback-obj-Precategory = pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)) - morphism-into-pullback-comm-pr1 : + comm-morphism-into-pr1-pullback-obj-Precategory : comp-hom-Precategory C pr1-pullback-obj-Precategory morphism-into-pullback-obj-Precategory ＝ p₁' - morphism-into-pullback-comm-pr1 = + comm-morphism-into-pr1-pullback-obj-Precategory = pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) - morphism-into-pullback-comm-pr2 : + comm-morphism-into-pr2-pullback-obj-Precategory : comp-hom-Precategory C pr2-pullback-obj-Precategory morphism-into-pullback-obj-Precategory ＝ p₂' - morphism-into-pullback-comm-pr2 = + comm-morphism-into-pr2-pullback-obj-Precategory = pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) is-unique-morphism-into-pullback-obj-Precategory : @@ -172,3 +172,8 @@ module _ pr2 is-pullback-prop-Precategory = is-prop-is-pullback-obj-Precategory ``` + +## See also + +- [Pushouts](category-theory.pushouts-in-precategories.md) for the dual + concept. diff --git a/src/category-theory/pushouts-in-precategories.lagda.md b/src/category-theory/pushouts-in-precategories.lagda.md new file mode 100644 index 0000000000..596a6bf6cd --- /dev/null +++ b/src/category-theory/pushouts-in-precategories.lagda.md @@ -0,0 +1,171 @@ +# Pushouts in precategories + +```agda +module category-theory.pushouts-in-precategories where +``` + +
Imports + +```agda +open import category-theory.precategories +open import category-theory.pullbacks-in-precategories +open import category-theory.opposite-precategories + +open import foundation.action-on-identifications-functions +open import foundation.cartesian-product-types +open import foundation.contractible-types +open import foundation.dependent-pair-types +open import foundation.identity-types +open import foundation.iterated-dependent-product-types +open import foundation.propositions +open import foundation.uniqueness-quantification +open import foundation.universe-levels +``` + +
+ +## Idea + +A +{{#concept "pushout" Disambiguation="of objects in precategories" Agda=pushout-obj-Precategory}} +of two morphisms `f : hom x y` and `g : hom x z` in a category `C` consists of: + +- an object `w` +- morphisms `i₁ : hom y w` and `i₂ : hom z w` such that +- `i₁ ∘ f` = i₂ ∘ g`` together with the universal property that for every object + `w'` and pair of morphisms `i₁' : hom y w'` and `i₂' : hom z w'` such that + `i₁' ∘ f = i₂' ∘ g` there exists a unique morphism `h : hom w w'` such that +- `h ∘ i₁ = i₁'` +- `h ∘ i₂ = i₂'`. + +We say that `C` +{{#concept "has all pushouts" Disambiguation="precategory" Agda=has-all-pushout-obj-Precategory}} +if there is a choice of a pushout for each object `x` and pair of morphisms +out of `x` in `C`. + +All definitions here are defined in terms of pullbacks in the [opposite precategory](category-theory.opposite-precategories.md); see [pullbacks](category-theory.pullbacks-in-precategories.md) for details. + +## Definition + +```agda +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + where + + is-pushout-obj-Precategory : + (x y z : obj-Precategory C) → + (f : hom-Precategory C x y) → + (g : hom-Precategory C x z) → + (w : obj-Precategory C) → + (i₁ : hom-Precategory C y w) → + (i₂ : hom-Precategory C z w) → + comp-hom-Precategory C i₁ f ＝ comp-hom-Precategory C i₂ g → + UU (l1 ⊔ l2) + is-pushout-obj-Precategory = + is-pullback-obj-Precategory (opposite-Precategory C) + + pushout-obj-Precategory : + (x y z : obj-Precategory C) → + hom-Precategory C x y → + hom-Precategory C x z → + UU (l1 ⊔ l2) + pushout-obj-Precategory = + pullback-obj-Precategory (opposite-Precategory C) + + has-all-pushout-obj-Precategory : UU (l1 ⊔ l2) + has-all-pushout-obj-Precategory = + has-all-pullback-obj-Precategory (opposite-Precategory C) + +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (t : has-all-pushout-obj-Precategory C) + (x y z : obj-Precategory C) + (f : hom-Precategory C x y) + (g : hom-Precategory C x z) + where + + object-pushout-obj-Precategory : obj-Precategory C + object-pushout-obj-Precategory = + object-pullback-obj-Precategory (opposite-Precategory C) t x y z f g + + inl-pushout-obj-Precategory : + hom-Precategory C y object-pushout-obj-Precategory + inl-pushout-obj-Precategory = + pr1-pullback-obj-Precategory (opposite-Precategory C) t x y z f g + + inr-pushout-obj-Precategory : + hom-Precategory C z object-pushout-obj-Precategory + inr-pushout-obj-Precategory = + pr2-pullback-obj-Precategory (opposite-Precategory C) t x y z f g + + comm-pushout-obj-Precategory : + comp-hom-Precategory C inl-pushout-obj-Precategory f ＝ + comp-hom-Precategory C inr-pushout-obj-Precategory g + comm-pushout-obj-Precategory = + comm-pullback-obj-Precategory (opposite-Precategory C) t x y z f g + + module _ + (w' : obj-Precategory C) + (i₁' : hom-Precategory C y w') + (i₂' : hom-Precategory C z w') + (α : comp-hom-Precategory C i₁' f ＝ comp-hom-Precategory C i₂' g) + where + + morphism-from-pushout-obj-Precategory : + hom-Precategory C object-pushout-obj-Precategory w' + morphism-from-pushout-obj-Precategory = + morphism-into-pullback-obj-Precategory (opposite-Precategory C) + t x y z f g w' i₁' i₂' α + + comm-morphism-into-inl-pushout-obj-Precategory : + comp-hom-Precategory C + morphism-from-pushout-obj-Precategory + inl-pushout-obj-Precategory ＝ + i₁' + comm-morphism-into-inl-pushout-obj-Precategory = + comm-morphism-into-pr1-pullback-obj-Precategory (opposite-Precategory C) + t x y z f g w' i₁' i₂' α + + comm-morphism-into-inr-pushout-obj-Precategory : + comp-hom-Precategory C + morphism-from-pushout-obj-Precategory + inr-pushout-obj-Precategory ＝ + i₂' + comm-morphism-into-inr-pushout-obj-Precategory = + comm-morphism-into-pr2-pullback-obj-Precategory (opposite-Precategory C) + t x y z f g w' i₁' i₂' α + + is-unique-morphism-from-pushout-obj-Precategory : + (h' : hom-Precategory C object-pushout-obj-Precategory w') → + comp-hom-Precategory C h' inl-pushout-obj-Precategory ＝ i₁' → + comp-hom-Precategory C h' inr-pushout-obj-Precategory ＝ i₂' → + morphism-from-pushout-obj-Precategory ＝ h' + is-unique-morphism-from-pushout-obj-Precategory = + is-unique-morphism-into-pullback-obj-Precategory (opposite-Precategory C) + t x y z f g w' i₁' i₂' α + +module _ + {l1 l2 : Level} (C : Precategory l1 l2) + (x y z : obj-Precategory C) + (f : hom-Precategory C x y) + (g : hom-Precategory C x z) + (w : obj-Precategory C) + (i₁ : hom-Precategory C y w) + (i₂ : hom-Precategory C z w) + (α : comp-hom-Precategory C i₁ f ＝ comp-hom-Precategory C i₂ g) + where + + is-prop-is-pushout-obj-Precategory : + is-prop (is-pushout-obj-Precategory C x y z f g w i₁ i₂ α) + is-prop-is-pushout-obj-Precategory = + is-prop-is-pullback-obj-Precategory (opposite-Precategory C) + x y z f g w i₁ i₂ α + + is-pushout-prop-Precategory : Prop (l1 ⊔ l2) + is-pushout-prop-Precategory = + is-pullback-prop-Precategory (opposite-Precategory C) x y z f g w i₁ i₂ α +``` + +## See also + +- [Pullbacks](category-theory.pullbacks-in-precategories.md) for the dual concept. From f118b61d9033f75c7ef1e1f2c5be00c1943346fd Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 10 Jun 2025 11:02:44 -0400 Subject: [PATCH 07/20] Pre-commit after adding the files --- src/category-theory.lagda.md | 1 + .../comonads-on-precategories.lagda.md | 3 +-- .../monads-on-precategories.lagda.md | 3 +-- .../pullbacks-in-precategories.lagda.md | 3 +-- .../pushouts-in-precategories.lagda.md | 20 +++++++++++-------- 5 files changed, 16 insertions(+), 14 deletions(-) diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index 2a908e4637..3a11ac3544 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -159,6 +159,7 @@ open import category-theory.products-in-precategories public open import category-theory.products-of-precategories public open import category-theory.pseudomonic-functors-precategories public open import category-theory.pullbacks-in-precategories public +open import category-theory.pushouts-in-precategories public open import category-theory.replete-subprecategories public open import category-theory.representable-functors-categories public open import category-theory.representable-functors-large-precategories public diff --git a/src/category-theory/comonads-on-precategories.lagda.md b/src/category-theory/comonads-on-precategories.lagda.md index 7fb283b76e..372923f5fa 100644 --- a/src/category-theory/comonads-on-precategories.lagda.md +++ b/src/category-theory/comonads-on-precategories.lagda.md @@ -449,5 +449,4 @@ module _ ## See also -- [Monads](category-theory.monads-on-precategories.md) for the dual - concept. +- [Monads](category-theory.monads-on-precategories.md) for the dual concept. diff --git a/src/category-theory/monads-on-precategories.lagda.md b/src/category-theory/monads-on-precategories.lagda.md index a51f7da56b..f0326b232d 100644 --- a/src/category-theory/monads-on-precategories.lagda.md +++ b/src/category-theory/monads-on-precategories.lagda.md @@ -443,5 +443,4 @@ module _ ## See also -- [Comonads](category-theory.comonads-on-precategories.md) for the dual - concept. +- [Comonads](category-theory.comonads-on-precategories.md) for the dual concept. diff --git a/src/category-theory/pullbacks-in-precategories.lagda.md b/src/category-theory/pullbacks-in-precategories.lagda.md index 49b7e958bd..4028c54a62 100644 --- a/src/category-theory/pullbacks-in-precategories.lagda.md +++ b/src/category-theory/pullbacks-in-precategories.lagda.md @@ -175,5 +175,4 @@ module _ ## See also -- [Pushouts](category-theory.pushouts-in-precategories.md) for the dual - concept. +- [Pushouts](category-theory.pushouts-in-precategories.md) for the dual concept. diff --git a/src/category-theory/pushouts-in-precategories.lagda.md b/src/category-theory/pushouts-in-precategories.lagda.md index 596a6bf6cd..6e8e889d89 100644 --- a/src/category-theory/pushouts-in-precategories.lagda.md +++ b/src/category-theory/pushouts-in-precategories.lagda.md @@ -7,9 +7,9 @@ module category-theory.pushouts-in-precategories where
Imports ```agda +open import category-theory.opposite-precategories open import category-theory.precategories open import category-theory.pullbacks-in-precategories -open import category-theory.opposite-precategories open import foundation.action-on-identifications-functions open import foundation.cartesian-product-types @@ -32,18 +32,21 @@ of two morphisms `f : hom x y` and `g : hom x z` in a category `C` consists of: - an object `w` - morphisms `i₁ : hom y w` and `i₂ : hom z w` such that -- `i₁ ∘ f` = i₂ ∘ g`` together with the universal property that for every object - `w'` and pair of morphisms `i₁' : hom y w'` and `i₂' : hom z w'` such that - `i₁' ∘ f = i₂' ∘ g` there exists a unique morphism `h : hom w w'` such that +- `i₁ ∘ f = i₂ ∘ g` together with the universal property that for every + object`w'` and pair of morphisms `i₁' : hom y w'` and `i₂' : hom z w'` such + that `i₁' ∘ f = i₂' ∘ g` there exists a unique morphism `h : hom w w'` such + that - `h ∘ i₁ = i₁'` - `h ∘ i₂ = i₂'`. We say that `C` {{#concept "has all pushouts" Disambiguation="precategory" Agda=has-all-pushout-obj-Precategory}} -if there is a choice of a pushout for each object `x` and pair of morphisms -out of `x` in `C`. +if there is a choice of a pushout for each object `x` and pair of morphisms out +of `x` in `C`. -All definitions here are defined in terms of pullbacks in the [opposite precategory](category-theory.opposite-precategories.md); see [pullbacks](category-theory.pullbacks-in-precategories.md) for details. +All definitions here are defined in terms of pullbacks in the +[opposite precategory](category-theory.opposite-precategories.md); see +[pullbacks](category-theory.pullbacks-in-precategories.md) for details. ## Definition @@ -168,4 +171,5 @@ module _ ## See also -- [Pullbacks](category-theory.pullbacks-in-precategories.md) for the dual concept. +- [Pullbacks](category-theory.pullbacks-in-precategories.md) for the dual + concept. From 24def73a555968d81d1d095713988d96822ad842 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 10 Jun 2025 13:36:51 -0400 Subject: [PATCH 08/20] Fix missed dualization in copointed description --- .../copointed-endofunctors-precategories.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/category-theory/copointed-endofunctors-precategories.lagda.md b/src/category-theory/copointed-endofunctors-precategories.lagda.md index da5e6667ff..d4845e11f0 100644 --- a/src/category-theory/copointed-endofunctors-precategories.lagda.md +++ b/src/category-theory/copointed-endofunctors-precategories.lagda.md @@ -25,8 +25,8 @@ An [endofunctor](category-theory.functors-precategories.md) `F : C → C` on a {{#concept "copointed" Disambiguation="endofunctor on a category" Agda=copointed-endofunctor-Precategory}} if it comes equipped with a [natural transformation](category-theory.natural-transformations-functors-precategories.md) -`id ⇒ F` from the identity [functor](category-theory.functors-precategories.md) -to `F`. +`F ⇒ id` from `F` to the identity +[functor](category-theory.functors-precategories.md). More explicitly, a {{#concept "copointing" Disambiguation="endofunctor on a precategory" Agda=copointing-endofunctor-Precategory}} From 9f97fc6b0ce7f035d0dc8beaebc5fbc3211ce30f Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 10 Jun 2025 14:13:41 -0400 Subject: [PATCH 09/20] Change lingering `into` to `from` in pushouts --- src/category-theory/pushouts-in-precategories.lagda.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/category-theory/pushouts-in-precategories.lagda.md b/src/category-theory/pushouts-in-precategories.lagda.md index 6e8e889d89..d3f874da9b 100644 --- a/src/category-theory/pushouts-in-precategories.lagda.md +++ b/src/category-theory/pushouts-in-precategories.lagda.md @@ -120,21 +120,21 @@ module _ morphism-into-pullback-obj-Precategory (opposite-Precategory C) t x y z f g w' i₁' i₂' α - comm-morphism-into-inl-pushout-obj-Precategory : + comm-morphism-from-inl-pushout-obj-Precategory : comp-hom-Precategory C morphism-from-pushout-obj-Precategory inl-pushout-obj-Precategory ＝ i₁' - comm-morphism-into-inl-pushout-obj-Precategory = + comm-morphism-from-inl-pushout-obj-Precategory = comm-morphism-into-pr1-pullback-obj-Precategory (opposite-Precategory C) t x y z f g w' i₁' i₂' α - comm-morphism-into-inr-pushout-obj-Precategory : + comm-morphism-from-inr-pushout-obj-Precategory : comp-hom-Precategory C morphism-from-pushout-obj-Precategory inr-pushout-obj-Precategory ＝ i₂' - comm-morphism-into-inr-pushout-obj-Precategory = + comm-morphism-from-inr-pushout-obj-Precategory = comm-morphism-into-pr2-pullback-obj-Precategory (opposite-Precategory C) t x y z f g w' i₁' i₂' α From 91ff2326779b9b97100122dd97e7a7d6ca33af08 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 10 Jun 2025 16:08:59 -0400 Subject: [PATCH 10/20] Typos; rename `is-(co)limiting` to `is-(co)limit` --- .../colimits-precategories.lagda.md | 28 +++++++++---------- .../limits-precategories.lagda.md | 28 +++++++++---------- ...ointed-endofunctors-precategories.lagda.md | 2 +- ...-algebras-monads-on-precategories.lagda.md | 6 ++-- ...lgebras-comonads-on-precategories.lagda.md | 6 ++-- src/foundation/category-of-sets.lagda.md | 8 +++--- 6 files changed, 39 insertions(+), 39 deletions(-) diff --git a/src/category-theory/colimits-precategories.lagda.md b/src/category-theory/colimits-precategories.lagda.md index 994a6648c2..cd54137166 100644 --- a/src/category-theory/colimits-precategories.lagda.md +++ b/src/category-theory/colimits-precategories.lagda.md @@ -63,16 +63,16 @@ module _ (F : functor-Precategory C D) where - is-colimiting-cocone-Precategory : + is-colimit-cocone-Precategory : cocone-Precategory C D F → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - is-colimiting-cocone-Precategory τ = + is-colimit-cocone-Precategory τ = (d : obj-Precategory D) → is-equiv (cocone-map-Precategory C D F τ d) colimit-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) colimit-Precategory = Σ ( cocone-Precategory C D F) - ( is-colimiting-cocone-Precategory) + ( is-colimit-cocone-Precategory) cocone-colimit-Precategory : colimit-Precategory → @@ -85,10 +85,10 @@ module _ vertex-colimit-Precategory τ = vertex-cocone-Precategory C D F (cocone-colimit-Precategory τ) - is-colimiting-colimit-Precategory : + is-colimit-colimit-Precategory : (τ : colimit-Precategory) → - is-colimiting-cocone-Precategory (cocone-colimit-Precategory τ) - is-colimiting-colimit-Precategory = pr2 + is-colimit-cocone-Precategory (cocone-colimit-Precategory τ) + is-colimit-colimit-Precategory = pr2 hom-cocone-colimit-Precategory : (τ : colimit-Precategory) → @@ -98,7 +98,7 @@ module _ ( vertex-cocone-Precategory C D F φ) hom-cocone-colimit-Precategory τ φ = map-inv-is-equiv - ( is-colimiting-colimit-Precategory τ + ( is-colimit-colimit-Precategory τ ( vertex-cocone-Precategory C D F φ)) ( natural-transformation-cocone-Precategory C D F φ) ``` @@ -153,10 +153,10 @@ module _ (F : functor-Precategory C D) where - is-prop-is-colimiting-cocone-Precategory : + is-prop-is-colimit-cocone-Precategory : (τ : cocone-Precategory C D F) → - is-prop (is-colimiting-cocone-Precategory C D F τ) - is-prop-is-colimiting-cocone-Precategory τ = + is-prop (is-colimit-cocone-Precategory C D F τ) + is-prop-is-colimit-cocone-Precategory τ = is-prop-Π λ φ → is-property-is-equiv _ is-prop-is-colimit-Precategory' : @@ -175,13 +175,13 @@ module _ (F : functor-Precategory C D) where - equiv-is-left-kan-extension-is-colimiting-Precategory : + equiv-is-left-kan-extension-is-colimit-Precategory : (τ : cocone-Precategory C D F) → - is-colimiting-cocone-Precategory C D F τ ≃ + is-colimit-cocone-Precategory C D F τ ≃ is-left-kan-extension-Precategory C terminal-Precategory D (terminal-functor-Precategory C) F (map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) - equiv-is-left-kan-extension-is-colimiting-Precategory τ = + equiv-is-left-kan-extension-is-colimit-Precategory τ = equiv-Π _ ( equiv-point-Precategory D) ( λ x → @@ -239,7 +239,7 @@ module _ ( is-left-kan-extension-Precategory C terminal-Precategory D ( terminal-functor-Precategory C) F) ( equiv-left-extension-cocone-Precategory C D F) - ( λ τ → equiv-is-left-kan-extension-is-colimiting-Precategory τ) + ( λ τ → equiv-is-left-kan-extension-is-colimit-Precategory τ) colimit-colimit'-Precategory : colimit-Precategory C D F → colimit-Precategory' C D F diff --git a/src/category-theory/limits-precategories.lagda.md b/src/category-theory/limits-precategories.lagda.md index 60015d9a58..338afac550 100644 --- a/src/category-theory/limits-precategories.lagda.md +++ b/src/category-theory/limits-precategories.lagda.md @@ -63,16 +63,16 @@ module _ (F : functor-Precategory C D) where - is-limiting-cone-Precategory : + is-limit-cone-Precategory : cone-Precategory C D F → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) - is-limiting-cone-Precategory τ = + is-limit-cone-Precategory τ = (d : obj-Precategory D) → is-equiv (cone-map-Precategory C D F τ d) limit-Precategory : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) limit-Precategory = Σ ( cone-Precategory C D F) - ( is-limiting-cone-Precategory) + ( is-limit-cone-Precategory) cone-limit-Precategory : limit-Precategory → @@ -85,10 +85,10 @@ module _ vertex-limit-Precategory τ = vertex-cone-Precategory C D F (cone-limit-Precategory τ) - is-limiting-limit-Precategory : + is-limit-limit-Precategory : (τ : limit-Precategory) → - is-limiting-cone-Precategory (cone-limit-Precategory τ) - is-limiting-limit-Precategory = pr2 + is-limit-cone-Precategory (cone-limit-Precategory τ) + is-limit-limit-Precategory = pr2 hom-cone-limit-Precategory : (τ : limit-Precategory) → @@ -98,7 +98,7 @@ module _ ( vertex-limit-Precategory τ) hom-cone-limit-Precategory τ φ = map-inv-is-equiv - ( is-limiting-limit-Precategory τ + ( is-limit-limit-Precategory τ ( vertex-cone-Precategory C D F φ)) ( natural-transformation-cone-Precategory C D F φ) ``` @@ -153,10 +153,10 @@ module _ (F : functor-Precategory C D) where - is-prop-is-limiting-cone-Precategory : + is-prop-is-limit-cone-Precategory : (τ : cone-Precategory C D F) → - is-prop (is-limiting-cone-Precategory C D F τ) - is-prop-is-limiting-cone-Precategory τ = + is-prop (is-limit-cone-Precategory C D F τ) + is-prop-is-limit-cone-Precategory τ = is-prop-Π λ φ → is-property-is-equiv _ is-prop-is-limit-Precategory' : @@ -175,13 +175,13 @@ module _ (F : functor-Precategory C D) where - equiv-is-right-kan-extension-is-limiting-Precategory : + equiv-is-right-kan-extension-is-limit-Precategory : (τ : cone-Precategory C D F) → - is-limiting-cone-Precategory C D F τ ≃ + is-limit-cone-Precategory C D F τ ≃ is-right-kan-extension-Precategory C terminal-Precategory D (terminal-functor-Precategory C) F (map-equiv (equiv-right-extension-cone-Precategory C D F) τ) - equiv-is-right-kan-extension-is-limiting-Precategory τ = + equiv-is-right-kan-extension-is-limit-Precategory τ = equiv-Π _ ( equiv-point-Precategory D) ( λ x → @@ -239,7 +239,7 @@ module _ ( is-right-kan-extension-Precategory C terminal-Precategory D ( terminal-functor-Precategory C) F) ( equiv-right-extension-cone-Precategory C D F) - ( λ τ → equiv-is-right-kan-extension-is-limiting-Precategory τ) + ( λ τ → equiv-is-right-kan-extension-is-limit-Precategory τ) limit-limit'-Precategory : limit-Precategory C D F → limit-Precategory' C D F diff --git a/src/category-theory/pointed-endofunctors-precategories.lagda.md b/src/category-theory/pointed-endofunctors-precategories.lagda.md index 453b5b4949..eb7d385f9e 100644 --- a/src/category-theory/pointed-endofunctors-precategories.lagda.md +++ b/src/category-theory/pointed-endofunctors-precategories.lagda.md @@ -142,5 +142,5 @@ module _ ## See also -- [Coointed endofunctors](category-theory.copointed-endofunctors-precategories.md) +- [Copointed endofunctors](category-theory.copointed-endofunctors-precategories.md) for the dual concept. diff --git a/src/category-theory/precategory-of-algebras-monads-on-precategories.lagda.md b/src/category-theory/precategory-of-algebras-monads-on-precategories.lagda.md index 1c991d8657..bd8572ad93 100644 --- a/src/category-theory/precategory-of-algebras-monads-on-precategories.lagda.md +++ b/src/category-theory/precategory-of-algebras-monads-on-precategories.lagda.md @@ -1,4 +1,4 @@ -# The precategory of algebras of a monad +# The precategory of algebras over a monad ```agda module category-theory.precategory-of-algebras-monads-on-precategories where @@ -35,8 +35,8 @@ open import foundation-core.transport-along-identifications ## Idea The -{{#concept "precategory of algebras" Disambiguation="of a monad on a precategory" Agda=algebras-monad-Precategory}} -of a [monad on a precategory](category-theory.monads-on-precategories.md) `T`, +{{#concept "precategory of algebras" Disambiguation="over a monad on a precategory" Agda=algebras-monad-Precategory}} +over a [monad on a precategory](category-theory.monads-on-precategories.md) `T`, denoted `EM(T)`, also called the **Eilenberg–Moore precategory**, consists of all `T`-algebras and `T`-algebra morphisms. It comes with an adjunction `C ⇄ EM(T)`. diff --git a/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md b/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md index 91466df096..6278cc21be 100644 --- a/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md +++ b/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md @@ -1,4 +1,4 @@ -# The precategory of coalgebras of a comonad +# The precategory of coalgebras over a comonad ```agda module category-theory.precategory-of-coalgebras-comonads-on-precategories where @@ -35,8 +35,8 @@ open import foundation-core.transport-along-identifications ## Idea The -{{#concept "precategory of coalgebras" Disambiguation="of a comonad on a precategory" Agda=coalgebras-comonad-Precategory}} -of a [comonad on a precategory](category-theory.comonads-on-precategories.md) +{{#concept "precategory of coalgebras" Disambiguation="over a comonad on a precategory" Agda=coalgebras-comonad-Precategory}} +over a [comonad on a precategory](category-theory.comonads-on-precategories.md) `T`, denoted `EM(T)`, also called the **Eilenberg–Moore precategory**, consists of all `T`-coalgebras and `T`-coalgebra morphisms. It comes with an adjunction `EM(T) ⇄ C`. diff --git a/src/foundation/category-of-sets.lagda.md b/src/foundation/category-of-sets.lagda.md index 7089fccb08..85c55098b9 100644 --- a/src/foundation/category-of-sets.lagda.md +++ b/src/foundation/category-of-sets.lagda.md @@ -239,10 +239,10 @@ module _ ( _) ( λ f → eq-htpy λ {(map-raise star) → refl}) - is-limiting-cone-Set-Precategory : - is-limiting-cone-Precategory C (Set-Precategory (l1 ⊔ l2)) F + is-limit-cone-Set-Precategory : + is-limit-cone-Precategory C (Set-Precategory (l1 ⊔ l2)) F cone-limit-Set-Precategory - is-limiting-cone-Set-Precategory φ = + is-limit-cone-Set-Precategory φ = is-equiv-is-invertible ( map-inv-cone-map-limit-Set-Precategory φ) ( is-section-cone-map-limit-Set-Precategory φ) @@ -251,7 +251,7 @@ module _ limit-Set-Precategory : limit-Precategory C (Set-Precategory (l1 ⊔ l2)) F pr1 limit-Set-Precategory = cone-limit-Set-Precategory - pr2 limit-Set-Precategory = is-limiting-cone-Set-Precategory + pr2 limit-Set-Precategory = is-limit-cone-Set-Precategory is-complete-Set-Precategory : (l1 l2 : Level) → From c0cff07ce61ac2f931d56842fe96e373b6d7bd17 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 17 Jun 2025 14:47:12 -0400 Subject: [PATCH 11/20] Apply suggestions from code review --- .../cocones-precategories.lagda.md | 8 +- .../colimits-precategories.lagda.md | 86 ++++++++++++------- .../cones-precategories.lagda.md | 8 +- .../limits-precategories.lagda.md | 83 +++++++++++------- 4 files changed, 116 insertions(+), 69 deletions(-) diff --git a/src/category-theory/cocones-precategories.lagda.md b/src/category-theory/cocones-precategories.lagda.md index 4216f4f5f0..e1ef57e5f8 100644 --- a/src/category-theory/cocones-precategories.lagda.md +++ b/src/category-theory/cocones-precategories.lagda.md @@ -165,11 +165,11 @@ module _ pr1 (cocone-map-Precategory τ d f) x = comp-hom-Precategory D f (component-cocone-Precategory τ x) pr2 (cocone-map-Precategory τ d f) h = - left-unit-law-comp-hom-Precategory D _ ∙ - ap + ( left-unit-law-comp-hom-Precategory D _) ∙ + ( ap ( λ g → comp-hom-Precategory D f g) - ( naturality-cocone-Precategory τ h) ∙ - inv (associative-comp-hom-Precategory D _ _ _) + ( naturality-cocone-Precategory τ h)) ∙ + ( inv (associative-comp-hom-Precategory D _ _ _)) ``` ## Properties diff --git a/src/category-theory/colimits-precategories.lagda.md b/src/category-theory/colimits-precategories.lagda.md index cd54137166..8d9f1319f9 100644 --- a/src/category-theory/colimits-precategories.lagda.md +++ b/src/category-theory/colimits-precategories.lagda.md @@ -28,6 +28,8 @@ open import foundation.propositions open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels + +open import foundation-core.homotopies ```
@@ -39,8 +41,8 @@ A of a [functor](category-theory.functors-precategories.md) `F` between [precategories](category-theory.precategories.md) is a colimiting [cocone](category-theory.cocones-precategories.md) under `F`. That is, a cocone -`τ` such that `cocone-map-Precategory C D F τ d` is an equivalence for all -`d : obj-Precategory D`. +`τ` such that `cocone-map-Precategory C D F τ d` is an +[equivalence](foundation-core.equivalences.md) for all `d : obj-Precategory D`. Equivalently, the colimit of `F` is a [left kan extension](category-theory.left-kan-extensions-precategories.md) of @@ -53,7 +55,7 @@ colimiting cocones as our official one. If a colimit exists, we call the vertex of the colimiting cocone the **vertex** of the colimit. -## Definition +## Definitions ### Colimiting cocones @@ -157,14 +159,14 @@ module _ (τ : cocone-Precategory C D F) → is-prop (is-colimit-cocone-Precategory C D F τ) is-prop-is-colimit-cocone-Precategory τ = - is-prop-Π λ φ → is-property-is-equiv _ + is-prop-Π (λ φ → is-property-is-equiv _) is-prop-is-colimit-Precategory' : ( R : left-extension-Precategory C terminal-Precategory D (terminal-functor-Precategory C) F) → is-prop (is-colimit-left-extension-Precategory C D F R) is-prop-is-colimit-Precategory' R = - is-prop-Π λ K → is-property-is-equiv _ + is-prop-Π (λ K → is-property-is-equiv _) ``` ### Colimiting cocones are equivalent to colimits @@ -178,9 +180,10 @@ module _ equiv-is-left-kan-extension-is-colimit-Precategory : (τ : cocone-Precategory C D F) → is-colimit-cocone-Precategory C D F τ ≃ - is-left-kan-extension-Precategory C terminal-Precategory D - (terminal-functor-Precategory C) F - (map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) + is-left-kan-extension-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) + ( F) + ( map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) equiv-is-left-kan-extension-is-colimit-Precategory τ = equiv-Π _ ( equiv-point-Precategory D) @@ -190,23 +193,41 @@ module _ ( is-property-is-equiv _) ( λ e → is-equiv-left-factor - ( induced-left-extension-map x) - ( natural-transformation-constant-functor-Precategory - terminal-Precategory D) - ( tr is-equiv (inv (lemma τ x)) e) - ( is-equiv-natural-transformation-constant-functor-Precategory - D _ _)) + ( induced-left-extension-map x) + ( natural-transformation-constant-functor-Precategory + ( terminal-Precategory) + ( D)) + ( tr is-equiv (inv (lemma τ x)) e) + ( is-equiv-natural-transformation-constant-functor-Precategory + ( D) + ( _) + ( _))) ( λ e → tr is-equiv (lemma τ x) ( is-equiv-comp ( induced-left-extension-map x) ( natural-transformation-constant-functor-Precategory - terminal-Precategory D) + ( terminal-Precategory) + ( D)) ( is-equiv-natural-transformation-constant-functor-Precategory - D _ _) + ( D) + ( _) + ( _)) ( e)))) where - induced-left-extension-map = λ x → + induced-left-extension-map : + ( x : obj-Precategory D) → + natural-transformation-Precategory terminal-Precategory D + ( extension-left-extension-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) + ( F) + ( map-equiv (equiv-left-extension-cocone-Precategory C D F) τ)) + ( constant-functor-Precategory terminal-Precategory D x) → + natural-transformation-Precategory C D F + ( comp-functor-Precategory C terminal-Precategory D + ( constant-functor-Precategory terminal-Precategory D x) + ( terminal-functor-Precategory C)) + induced-left-extension-map x = left-extension-map-Precategory C terminal-Precategory D ( terminal-functor-Precategory C) ( F) ( map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) @@ -214,23 +235,24 @@ module _ lemma : ( τ : cocone-Precategory C D F) ( x : obj-Precategory D) → - ( left-extension-map-Precategory C terminal-Precategory D - ( terminal-functor-Precategory C) F - ( map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) - ( constant-functor-Precategory terminal-Precategory D x)) ∘ - ( natural-transformation-constant-functor-Precategory - terminal-Precategory D) ＝ + ( left-extension-map-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) F + ( map-equiv (equiv-left-extension-cocone-Precategory C D F) τ) + ( constant-functor-Precategory terminal-Precategory D x)) ∘ + ( natural-transformation-constant-functor-Precategory + terminal-Precategory D) ＝ ( cocone-map-Precategory C D F τ x) lemma τ x = - eq-htpy λ f → - eq-htpy-hom-family-natural-transformation-Precategory C D - ( F) - ( comp-functor-Precategory C terminal-Precategory D - ( point-Precategory D x) - ( terminal-functor-Precategory C)) - ( _) - ( _) - ( λ g → refl) + eq-htpy + ( λ f → + eq-htpy-hom-family-natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C terminal-Precategory D + ( point-Precategory D x) + ( terminal-functor-Precategory C)) + ( _) + ( _) + ( refl-htpy)) equiv-colimit-colimit'-Precategory : colimit-Precategory C D F ≃ colimit-Precategory' C D F diff --git a/src/category-theory/cones-precategories.lagda.md b/src/category-theory/cones-precategories.lagda.md index 12df81dc10..b041ffe0da 100644 --- a/src/category-theory/cones-precategories.lagda.md +++ b/src/category-theory/cones-precategories.lagda.md @@ -166,11 +166,11 @@ module _ pr1 (cone-map-Precategory τ d f) x = comp-hom-Precategory D (component-cone-Precategory τ x) f pr2 (cone-map-Precategory τ d f) h = - inv (associative-comp-hom-Precategory D _ _ _) ∙ - ap + ( inv (associative-comp-hom-Precategory D _ _ _)) ∙ + ( ap ( λ g → comp-hom-Precategory D g f) - ( inv (naturality-cone-Precategory τ h)) ∙ - inv (right-unit-law-comp-hom-Precategory D _) + ( inv (naturality-cone-Precategory τ h))) ∙ + ( inv (right-unit-law-comp-hom-Precategory D _)) ``` ## Properties diff --git a/src/category-theory/limits-precategories.lagda.md b/src/category-theory/limits-precategories.lagda.md index 338afac550..9ba2e995ab 100644 --- a/src/category-theory/limits-precategories.lagda.md +++ b/src/category-theory/limits-precategories.lagda.md @@ -28,6 +28,8 @@ open import foundation.propositions open import foundation.transport-along-identifications open import foundation.unit-type open import foundation.universe-levels + +open import foundation-core.homotopies ``` @@ -39,8 +41,8 @@ A of a [functor](category-theory.functors-precategories.md) `F` between [precategories](category-theory.precategories.md) is a limiting [cone](category-theory.cones-precategories.md) over `F`. That is, a cone `τ` -such that `cone-map-Precategory C D F τ d` is an equivalence for all -`d : obj-Precategory D`. +such that `cone-map-Precategory C D F τ d` is an +[equivalence](foundation-core.equivalences.md) for all `d : obj-Precategory D`. Equivalently, the limit of `F` is a [right kan extension](category-theory.right-kan-extensions-precategories.md) of @@ -53,7 +55,7 @@ limiting cones as our official one. If a limit exists, we call the vertex of the limiting cone the **vertex** of the limit. -## Definition +## Definitions ### Limiting cones @@ -157,14 +159,14 @@ module _ (τ : cone-Precategory C D F) → is-prop (is-limit-cone-Precategory C D F τ) is-prop-is-limit-cone-Precategory τ = - is-prop-Π λ φ → is-property-is-equiv _ + is-prop-Π (λ φ → is-property-is-equiv _) is-prop-is-limit-Precategory' : ( R : right-extension-Precategory C terminal-Precategory D (terminal-functor-Precategory C) F) → is-prop (is-limit-right-extension-Precategory C D F R) is-prop-is-limit-Precategory' R = - is-prop-Π λ K → is-property-is-equiv _ + is-prop-Π (λ K → is-property-is-equiv _) ``` ### Limiting cones are equivalent to limits @@ -178,9 +180,10 @@ module _ equiv-is-right-kan-extension-is-limit-Precategory : (τ : cone-Precategory C D F) → is-limit-cone-Precategory C D F τ ≃ - is-right-kan-extension-Precategory C terminal-Precategory D - (terminal-functor-Precategory C) F - (map-equiv (equiv-right-extension-cone-Precategory C D F) τ) + is-right-kan-extension-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) + ( F) + ( map-equiv (equiv-right-extension-cone-Precategory C D F) τ) equiv-is-right-kan-extension-is-limit-Precategory τ = equiv-Π _ ( equiv-point-Precategory D) @@ -192,45 +195,67 @@ module _ is-equiv-left-factor ( induced-right-extension-map x) ( natural-transformation-constant-functor-Precategory - terminal-Precategory D) + ( terminal-Precategory) + ( D)) ( tr is-equiv (inv (lemma τ x)) e) ( is-equiv-natural-transformation-constant-functor-Precategory - D _ _)) + ( D) + ( _) + ( _))) ( λ e → tr is-equiv (lemma τ x) ( is-equiv-comp ( induced-right-extension-map x) ( natural-transformation-constant-functor-Precategory - terminal-Precategory D) + ( terminal-Precategory) + ( D)) ( is-equiv-natural-transformation-constant-functor-Precategory - D _ _) + ( D) + ( _) + ( _)) ( e)))) where - induced-right-extension-map = λ x → + induced-right-extension-map : + ( x : obj-Precategory D) → + natural-transformation-Precategory terminal-Precategory D + ( constant-functor-Precategory terminal-Precategory D x) + ( extension-right-extension-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) + ( F) + ( map-equiv (equiv-right-extension-cone-Precategory C D F) τ)) → + natural-transformation-Precategory C D + ( comp-functor-Precategory C terminal-Precategory D + ( constant-functor-Precategory terminal-Precategory D x) + ( terminal-functor-Precategory C)) + ( F) + induced-right-extension-map x = right-extension-map-Precategory C terminal-Precategory D - ( terminal-functor-Precategory C) ( F) + ( terminal-functor-Precategory C) + ( F) ( map-equiv (equiv-right-extension-cone-Precategory C D F) τ) ( constant-functor-Precategory terminal-Precategory D x) lemma : ( τ : cone-Precategory C D F) ( x : obj-Precategory D) → - ( right-extension-map-Precategory C terminal-Precategory D - ( terminal-functor-Precategory C) F - ( map-equiv (equiv-right-extension-cone-Precategory C D F) τ) - ( constant-functor-Precategory terminal-Precategory D x)) ∘ - ( natural-transformation-constant-functor-Precategory - terminal-Precategory D) ＝ + ( right-extension-map-Precategory C terminal-Precategory D + ( terminal-functor-Precategory C) F + ( map-equiv (equiv-right-extension-cone-Precategory C D F) τ) + ( constant-functor-Precategory terminal-Precategory D x)) ∘ + ( natural-transformation-constant-functor-Precategory + ( terminal-Precategory) + ( D)) ＝ ( cone-map-Precategory C D F τ x) lemma τ x = - eq-htpy λ f → - eq-htpy-hom-family-natural-transformation-Precategory C D - ( comp-functor-Precategory C terminal-Precategory D - ( point-Precategory D x) - ( terminal-functor-Precategory C)) - ( F) - ( _) - ( _) - ( λ g → refl) + eq-htpy + ( λ f → + eq-htpy-hom-family-natural-transformation-Precategory C D + ( comp-functor-Precategory C terminal-Precategory D + ( point-Precategory D x) + ( terminal-functor-Precategory C)) + ( F) + ( _) + ( _) + ( refl-htpy)) equiv-limit-limit'-Precategory : limit-Precategory C D F ≃ limit-Precategory' C D F From fbb8194f37bd745881c17c0b0f0f404e1d08473f Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 17 Jun 2025 15:39:49 -0400 Subject: [PATCH 12/20] Dualize codensity monads --- src/category-theory.lagda.md | 1 + ...codensity-monads-on-precategories.lagda.md | 24 +- ...density-comonads-on-precategories.lagda.md | 592 ++++++++++++++++++ .../left-extensions-precategories.lagda.md | 4 +- 4 files changed, 606 insertions(+), 15 deletions(-) create mode 100644 src/category-theory/density-comonads-on-precategories.lagda.md diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index ec0437e7cc..5d61fc3b57 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -46,6 +46,7 @@ open import category-theory.coproducts-in-precategories public open import category-theory.cores-categories public open import category-theory.cores-precategories public open import category-theory.coslice-precategories public +open import category-theory.density-comonads-on-precategories public open import category-theory.dependent-composition-operations-over-precategories public open import category-theory.dependent-products-of-categories public open import category-theory.dependent-products-of-large-categories public diff --git a/src/category-theory/codensity-monads-on-precategories.lagda.md b/src/category-theory/codensity-monads-on-precategories.lagda.md index f02e0863b5..01ae7df622 100644 --- a/src/category-theory/codensity-monads-on-precategories.lagda.md +++ b/src/category-theory/codensity-monads-on-precategories.lagda.md @@ -177,10 +177,7 @@ module _ ( _) ( _)) ∙ ( ap - ( λ x → - ( comp-natural-transformation-Precategory C D RF RF F - ( α) - ( x))) + ( comp-natural-transformation-Precategory C D RF RF F α) ( inv ( preserves-comp-left-whisker-natural-transformation-Precategory ( C) @@ -205,10 +202,7 @@ module _ ( x)))) ( compute-unit-codensity-monad-Precategory C D F Rk)) ∙ ( ap - ( λ x → - ( comp-natural-transformation-Precategory C D RF RF F - ( α) - ( x))) + ( comp-natural-transformation-Precategory C D RF RF F α) ( preserves-id-left-whisker-natural-transformation-Precategory C D D ( F) ( R))) ∙ @@ -303,7 +297,7 @@ module _ ( _) ( _)) ∙ ( ap - ( λ x → comp-natural-transformation-Precategory C D RF RF F α x) + ( comp-natural-transformation-Precategory C D RF RF F α) ( eq-htpy-hom-family-natural-transformation-Precategory C D RF RF _ _ ( λ x → ( naturality-natural-transformation-Precategory D D @@ -393,7 +387,7 @@ module _ ( α)))) left-precomp-associative-mul-codensity-monad-Precategory = ( ap - ( λ x → comp-natural-transformation-Precategory C D RRRF RF F α x) + ( comp-natural-transformation-Precategory C D RRRF RF F α) ( preserves-comp-right-whisker-natural-transformation-Precategory D D C ( RRR) ( RR) @@ -429,7 +423,7 @@ module _ ( _) ( _)) ∙ ( ap - ( λ x → comp-natural-transformation-Precategory C D RRRF RF F α x) + ( comp-natural-transformation-Precategory C D RRRF RF F α) ( inv ( preserves-comp-left-whisker-natural-transformation-Precategory C D D ( RRF) @@ -479,7 +473,7 @@ module _ ( α)))) right-precomp-associative-mul-codensity-monad-Precategory = ( ap - ( λ x → comp-natural-transformation-Precategory C D RRRF RF F α x) + ( comp-natural-transformation-Precategory C D RRRF RF F α) ( preserves-comp-right-whisker-natural-transformation-Precategory D D C ( RRR) ( RR) @@ -547,7 +541,7 @@ module _ ( _) ( _)) ∙ ( ap - ( λ x → comp-natural-transformation-Precategory C D RRRF RF F α x) + ( comp-natural-transformation-Precategory C D RRRF RF F α) ( inv ( preserves-comp-left-whisker-natural-transformation-Precategory C D D ( RRF) @@ -602,6 +596,10 @@ module _ ( right-unit-law-mul-codensity-monad-Precategory C D F Rk))) ``` +## See also + +- [Codensity monad](codensity-monads-on-precategories.md) for the dual concept + ## External links - [Codensity monad](https://ncatlab.org/nlab/show/codensity+monad) at $n$Lab diff --git a/src/category-theory/density-comonads-on-precategories.lagda.md b/src/category-theory/density-comonads-on-precategories.lagda.md new file mode 100644 index 0000000000..526e3d7da1 --- /dev/null +++ b/src/category-theory/density-comonads-on-precategories.lagda.md @@ -0,0 +1,592 @@ +# Density comonads in precategories + +```agda +module category-theory.density-comonads-on-precategories where +``` + +
Imports + +```agda +open import category-theory.coalgebras-comonads-on-precategories +open import category-theory.comonads-on-precategories +open import category-theory.functors-precategories +open import category-theory.left-extensions-precategories +open import category-theory.left-kan-extensions-precategories +open import category-theory.natural-transformations-functors-precategories +open import category-theory.precategories + +open import foundation.action-on-identifications-functions +open import foundation.dependent-pair-types +open import foundation.equivalences +open import foundation.identity-types +open import foundation.universe-levels +``` + +
+ +## Idea + +Given an arbitrary [functor](category-theory.functors-precategories.md) +`F : C → D`, any [left Kan +extension](category-theory.left-kan-extensions-precategories.md] `L` of `F` +along itself `F` has a canonical +[comonad](category-theory.comonads-on-precategories.md] structure, called the +{{#concept "density comonad" Agda=density-comonad-Precategory}} of `L`. + +## Comonad structure + +The counit and comultiplication of the density comonads follow from the +"existence" part of the universal property of the right Kan extension. We use +two right extensions: the identity map on `D` trivially gives a right extension +of `D` along itself, and `L²` gives an extension by whiskering and composing the +natural transformation. By the universal property of `L`, these give natural +transformations `η : id ⇒ L` and `μ : L² ⇒ L`, respectively. From their +definition via the universal property, we have two computation rules for these +natural transformations (where ∙ is whiskering): + +1. `α ∘ (η ∙ F) ＝ id_F`; and +2. `α ∘ (μ ∙ F) = α ∘ (L ∙ α)`. + +```agda +module _ + {l1 l2 l3 l4 : Level} + (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + (Lk : left-kan-extension-Precategory C D D F F) + (let L = extension-left-kan-extension-Precategory C D D F F Lk) + (let KL = is-left-kan-extension-left-kan-extension-Precategory C D D F F Lk) + (let α = natural-transformation-left-kan-extension-Precategory C D D F F Lk) + (let LL = comp-functor-Precategory D D D L L) + (let LF = comp-functor-Precategory C D D L F) + (let LLF = comp-functor-Precategory C D D LL F) + where + + counit-density-comonad-Precategory : + natural-transformation-Precategory D D L (id-functor-Precategory D) + counit-density-comonad-Precategory = + map-inv-is-equiv + ( KL (id-functor-Precategory D)) + ( pr2 (id-left-extension-Precategory C D F)) + + abstract + compute-counit-density-comonad-Precategory : + comp-natural-transformation-Precategory C D F LF F + ( right-whisker-natural-transformation-Precategory D D C + ( L) + ( id-functor-Precategory D) + ( counit-density-comonad-Precategory) + ( F)) + ( α) ＝ + id-natural-transformation-Precategory C D F + compute-counit-density-comonad-Precategory = + is-section-map-inv-is-equiv (KL _) _ + + comul-density-comonad-Precategory : + natural-transformation-Precategory D D + ( L) + ( comp-functor-Precategory D D D L L) + comul-density-comonad-Precategory = + map-inv-is-equiv + ( KL (comp-functor-Precategory D D D L L)) + ( pr2 + ( square-left-extension-Precategory C D F + ( left-extension-left-kan-extension-Precategory C D D F F Lk))) + + abstract + compute-comul-density-comonad-Precategory : + comp-natural-transformation-Precategory C D F LF LLF + ( right-whisker-natural-transformation-Precategory D D C + ( L) + ( LL) + ( comul-density-comonad-Precategory) + ( F)) + ( α) ＝ + comp-natural-transformation-Precategory C D F LF LLF + ( left-whisker-natural-transformation-Precategory C D D + ( F) + ( LF) + ( L) + ( α)) + ( α) + compute-comul-density-comonad-Precategory = + is-section-map-inv-is-equiv (KL _) _ +``` + +## Comonad laws + +Comonad laws follow from the "uniqueness" part of the right Kan extension. + +### Left counit law + +For the left counit law, if `α : L∘F ⇒ F` is the right Kan extension natural +transformation, we show that the composite + +```text + (Lμ)F μF α + L∘F ⇒ L²∘F ⇒ L∘F ⇒ L +``` + +is equal to `α`; by uniqueness, `μF ∘ LμF = id`. + +```agda +module _ + {l1 l2 l3 l4 : Level} + (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + (Lk : left-kan-extension-Precategory C D D F F) + (let L = extension-left-kan-extension-Precategory C D D F F Lk) + (let KL = is-left-kan-extension-left-kan-extension-Precategory C D D F F Lk) + (let α = natural-transformation-left-kan-extension-Precategory C D D F F Lk) + (let LL = comp-functor-Precategory D D D L L) + (let LF = comp-functor-Precategory C D D L F) + (let LLF = comp-functor-Precategory C D D LL F) + where + + precomp-left-counit-law-comul-density-comonad-Precategory : + left-extension-map-Precategory C D D F F (L , α) L + ( comp-natural-transformation-Precategory + D D L LL L + ( left-whisker-natural-transformation-Precategory D D D + ( L) + ( id-functor-Precategory D) + ( L) + ( counit-density-comonad-Precategory C D F Lk)) + ( comul-density-comonad-Precategory C D F Lk)) ＝ + α + precomp-left-counit-law-comul-density-comonad-Precategory = + ( associative-comp-natural-transformation-Precategory C D F LF LLF LF + ( _) + ( _) + ( _)) ∙ + ( ap + ( λ x → + comp-natural-transformation-Precategory C D F LLF LF + ( right-whisker-natural-transformation-Precategory D D C LL L + ( left-whisker-natural-transformation-Precategory D D D + ( L) + ( id-functor-Precategory D) + ( L) + ( counit-density-comonad-Precategory C D F Lk)) + ( F)) + ( x)) + ( compute-comul-density-comonad-Precategory C D F Lk)) ∙ + ( inv + ( associative-comp-natural-transformation-Precategory C D F LF LLF LF + ( _) + ( _) + ( _))) ∙ + ( ap + ( λ x → + ( comp-natural-transformation-Precategory C D F LF LF + ( x) + ( α))) + ( inv + ( preserves-comp-left-whisker-natural-transformation-Precategory + ( C) + ( D) + ( D) + ( F) + ( LF) + ( F) + ( L) + ( right-whisker-natural-transformation-Precategory D D C + ( L) + ( id-functor-Precategory D) + ( counit-density-comonad-Precategory C D F Lk) + ( F)) + ( α)))) ∙ + ( ap + ( λ x → + ( comp-natural-transformation-Precategory C D F LF LF + ( left-whisker-natural-transformation-Precategory C D D F F + ( L) + ( x)) + ( α))) + ( compute-counit-density-comonad-Precategory C D F Lk)) ∙ + ( ap + ( λ x → + ( comp-natural-transformation-Precategory C D F LF LF + ( x) + ( α))) + ( preserves-id-left-whisker-natural-transformation-Precategory C D D + ( F) + ( L))) ∙ + ( left-unit-law-comp-natural-transformation-Precategory C D F LF α) + + abstract + left-counit-law-comul-density-comonad-Precategory : + comp-natural-transformation-Precategory + D D L (comp-functor-Precategory D D D L L) L + ( left-whisker-natural-transformation-Precategory D D D + ( L) + ( id-functor-Precategory D) + ( L) + ( counit-density-comonad-Precategory C D F Lk)) + ( comul-density-comonad-Precategory C D F Lk) ＝ + id-natural-transformation-Precategory D D L + left-counit-law-comul-density-comonad-Precategory = + ( inv (is-retraction-map-inv-is-equiv (KL L) _)) ∙ + ( ap + ( map-inv-is-equiv (KL L)) + ( ( precomp-left-counit-law-comul-density-comonad-Precategory) ∙ + ( inv + ( left-unit-law-comp-natural-transformation-Precategory C D + ( F) + ( LF) + ( α))))) ∙ + ( is-retraction-map-inv-is-equiv (KL L) _) +``` + +### Right counit law + +The right counit law is similar; we show that the composite is `α` via: + +```text + ηLF μF α + LF ⇒ L²F ⇒ LF ⇒ F + α ⇓ Lα ⇓ ∥ + F ⇒ LF ⇒ F + ηF α +``` + +The right square (triangle) commutes by "uniqueness" of the right Kan UP; the +left square commutes by naturality of `η`. The bottom composite is then `id` by +the UP again. + +```agda +module _ + {l1 l2 l3 l4 : Level} + (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + (Lk : left-kan-extension-Precategory C D D F F) + (let L = extension-left-kan-extension-Precategory C D D F F Lk) + (let KL = is-left-kan-extension-left-kan-extension-Precategory C D D F F Lk) + (let α = natural-transformation-left-kan-extension-Precategory C D D F F Lk) + (let LL = comp-functor-Precategory D D D L L) + (let LF = comp-functor-Precategory C D D L F) + (let LLF = comp-functor-Precategory C D D LL F) + where + + precomp-right-counit-law-comul-density-comonad-Precategory : + left-extension-map-Precategory C D D F F (L , α) L + ( comp-natural-transformation-Precategory + D D L LL L + ( right-whisker-natural-transformation-Precategory D D D + ( L) + ( id-functor-Precategory D) + ( counit-density-comonad-Precategory C D F Lk) + ( L)) + ( comul-density-comonad-Precategory C D F Lk)) ＝ + α + precomp-right-counit-law-comul-density-comonad-Precategory = + ( associative-comp-natural-transformation-Precategory C D F LF LLF LF + ( _) + ( _) + ( _)) ∙ + ( ap + ( comp-natural-transformation-Precategory C D F LLF LF + ( right-whisker-natural-transformation-Precategory D D C LL L + ( right-whisker-natural-transformation-Precategory D D D + ( L) + ( id-functor-Precategory D) + ( counit-density-comonad-Precategory C D F Lk) + ( L)) + ( F))) + ( is-section-map-inv-is-equiv + ( KL (comp-functor-Precategory D D D L L)) _)) ∙ + ( inv + ( associative-comp-natural-transformation-Precategory C D F LF LLF LF + ( _) + ( _) + ( _))) ∙ + ( ap + ( λ x → comp-natural-transformation-Precategory C D F LF LF x α) + ( eq-htpy-hom-family-natural-transformation-Precategory C D LF LF _ _ + (λ x → + inv + ( naturality-natural-transformation-Precategory D D + ( L) + ( id-functor-Precategory D) + ( counit-density-comonad-Precategory C D F Lk) + ( _))))) ∙ + ( associative-comp-natural-transformation-Precategory C D F LF F LF + ( _) + ( _) + ( _)) ∙ + ( ap + ( comp-natural-transformation-Precategory C D F F LF α) + ( compute-counit-density-comonad-Precategory C D F Lk)) ∙ + right-unit-law-comp-natural-transformation-Precategory C D F LF α + + abstract + right-counit-law-comul-density-comonad-Precategory : + comp-natural-transformation-Precategory + D D L (comp-functor-Precategory D D D L L) L + ( right-whisker-natural-transformation-Precategory D D D + ( L) + ( id-functor-Precategory D) + ( counit-density-comonad-Precategory C D F Lk) + ( L)) + ( comul-density-comonad-Precategory C D F Lk) ＝ + id-natural-transformation-Precategory D D L + right-counit-law-comul-density-comonad-Precategory = + ( inv (is-retraction-map-inv-is-equiv (KL L) _)) ∙ + ( ap + ( map-inv-is-equiv (KL L)) + ( ( precomp-right-counit-law-comul-density-comonad-Precategory) ∙ + ( inv + ( left-unit-law-comp-natural-transformation-Precategory C D + ( F) + ( LF) + ( α))))) ∙ + ( is-retraction-map-inv-is-equiv (KL L) _) +``` + +### Comultiplication is associative + +Showing that comultiplication is associative is similar but longer. + +```agda +module _ + {l1 l2 l3 l4 : Level} + (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + (Lk : left-kan-extension-Precategory C D D F F) + (let L = extension-left-kan-extension-Precategory C D D F F Lk) + (let KL = is-left-kan-extension-left-kan-extension-Precategory C D D F F Lk) + (let α = natural-transformation-left-kan-extension-Precategory C D D F F Lk) + (let LL = comp-functor-Precategory D D D L L) + (let LF = comp-functor-Precategory C D D L F) + (let LLF = comp-functor-Precategory C D D LL F) + (let LLL = comp-functor-Precategory D D D L LL) + (let LLLF = comp-functor-Precategory C D D LLL F) + where + + left-precomp-associative-comul-density-comonad-Precategory : + comp-natural-transformation-Precategory C D F LF LLLF + ( right-whisker-natural-transformation-Precategory D D C + ( L) + ( LLL) + ( comp-natural-transformation-Precategory D D L LL LLL + ( left-whisker-natural-transformation-Precategory D D D L LL + ( L) + ( comul-density-comonad-Precategory C D F Lk)) + ( comul-density-comonad-Precategory C D F Lk)) + ( F)) + ( α) ＝ + comp-natural-transformation-Precategory C D F LF LLLF + ( left-whisker-natural-transformation-Precategory C D D + ( F) + ( LLF) + ( L) + ( comp-natural-transformation-Precategory C D F LF LLF + ( left-whisker-natural-transformation-Precategory C D D + ( F) + ( LF) + ( L) + ( α)) + ( α))) + ( α) + left-precomp-associative-comul-density-comonad-Precategory = + ( ap + ( λ x → comp-natural-transformation-Precategory C D F LF LLLF x α) + ( preserves-comp-right-whisker-natural-transformation-Precategory D D C + ( L) + ( LL) + ( LLL) + ( left-whisker-natural-transformation-Precategory D D D L LL + ( L) + ( comul-density-comonad-Precategory C D F Lk)) + ( comul-density-comonad-Precategory C D F Lk) + ( F))) ∙ + ( associative-comp-natural-transformation-Precategory C D F LF LLF LLLF + ( _) + ( _) + ( _)) ∙ + ( ap + ( comp-natural-transformation-Precategory C D F LLF LLLF + ( right-whisker-natural-transformation-Precategory D D C + ( LL) + ( LLL) + ( left-whisker-natural-transformation-Precategory D D D L LL + ( L) + ( comul-density-comonad-Precategory C D F Lk)) + ( F))) + ( compute-comul-density-comonad-Precategory C D F Lk)) ∙ + ( inv + ( associative-comp-natural-transformation-Precategory C D F LF LLF LLLF + ( _) + ( _) + ( _))) ∙ + ( ap + ( λ x → comp-natural-transformation-Precategory C D F LF LLLF x α) + ( inv + ( preserves-comp-left-whisker-natural-transformation-Precategory C D D + ( F) + ( LF) + ( LLF) + ( L) + ( right-whisker-natural-transformation-Precategory D D C + ( L) + ( LL) + ( comul-density-comonad-Precategory C D F Lk) + ( F)) + ( α)))) ∙ + ( ap + ( λ x → comp-natural-transformation-Precategory C D F LF LLLF + ( left-whisker-natural-transformation-Precategory C D D + ( F) + ( LLF) + ( L) + ( x)) + ( α)) + ( compute-comul-density-comonad-Precategory C D F Lk)) + + right-precomp-associative-comul-density-comonad-Precategory : + comp-natural-transformation-Precategory C D F LF LLLF + ( right-whisker-natural-transformation-Precategory D D C + ( L) + ( LLL) + ( comp-natural-transformation-Precategory D D L LL LLL + ( right-whisker-natural-transformation-Precategory D D D L LL + ( comul-density-comonad-Precategory C D F Lk) + ( L)) + ( comul-density-comonad-Precategory C D F Lk)) + ( F)) + ( α) ＝ + comp-natural-transformation-Precategory C D F LF LLLF + ( left-whisker-natural-transformation-Precategory C D D + ( F) + ( LLF) + ( L) + ( comp-natural-transformation-Precategory C D F LF LLF + ( left-whisker-natural-transformation-Precategory C D D + ( F) + ( LF) + ( L) + ( α)) + ( α))) + ( α) + right-precomp-associative-comul-density-comonad-Precategory = + ( ap + ( λ x → comp-natural-transformation-Precategory C D F LF LLLF x α) + ( preserves-comp-right-whisker-natural-transformation-Precategory D D C + ( L) + ( LL) + ( LLL) + ( right-whisker-natural-transformation-Precategory D D D L LL + ( comul-density-comonad-Precategory C D F Lk) + ( L)) + ( comul-density-comonad-Precategory C D F Lk) + ( F))) ∙ + ( associative-comp-natural-transformation-Precategory C D F LF LLF LLLF + ( _) + ( _) + ( _)) ∙ + ( ap + ( comp-natural-transformation-Precategory C D F LLF LLLF + ( right-whisker-natural-transformation-Precategory D D C + ( LL) + ( LLL) + ( right-whisker-natural-transformation-Precategory D D D L LL + ( comul-density-comonad-Precategory C D F Lk) + ( L)) + ( F))) + ( compute-comul-density-comonad-Precategory C D F Lk)) ∙ + ( inv + ( associative-comp-natural-transformation-Precategory C D F LF LLF LLLF + ( _) + ( _) + ( _))) ∙ + ( ap + ( λ x → comp-natural-transformation-Precategory C D F LF LLLF x α) + ( eq-htpy-hom-family-natural-transformation-Precategory C D LF LLLF + ( _) + ( _) + ( λ x → + inv + ( naturality-natural-transformation-Precategory D D L LL + ( comul-density-comonad-Precategory C D F Lk) + ( _))))) ∙ + ( associative-comp-natural-transformation-Precategory C D F LF LLF LLLF + ( _) + ( _) + ( _)) ∙ + ( ap + ( λ x → + ( comp-natural-transformation-Precategory C D F LLF LLLF + ( left-whisker-natural-transformation-Precategory C D D + ( LF) + ( LLF) + ( L) + ( left-whisker-natural-transformation-Precategory C D D + ( F) + ( LF) + ( L) + ( α))) + ( x))) + ( compute-comul-density-comonad-Precategory C D F Lk)) ∙ + ( inv + ( associative-comp-natural-transformation-Precategory C D F LF LLF LLLF + ( _) + ( _) + ( _))) ∙ + ( ap + ( λ x → comp-natural-transformation-Precategory C D F LF LLLF x α) + ( inv + ( preserves-comp-left-whisker-natural-transformation-Precategory C D D + ( F) + ( LF) + ( LLF) + ( L) + ( left-whisker-natural-transformation-Precategory C D D + ( F) + ( LF) + ( L) + ( α)) + ( α)))) + + abstract + associative-comul-density-comonad-Precategory : + comp-natural-transformation-Precategory D D L LL LLL + ( left-whisker-natural-transformation-Precategory D D D L LL + ( L) + ( comul-density-comonad-Precategory C D F Lk)) + ( comul-density-comonad-Precategory C D F Lk) ＝ + comp-natural-transformation-Precategory D D L LL LLL + ( right-whisker-natural-transformation-Precategory D D D L LL + ( comul-density-comonad-Precategory C D F Lk) + ( L)) + ( comul-density-comonad-Precategory C D F Lk) + associative-comul-density-comonad-Precategory = + ( inv (is-retraction-map-inv-is-equiv (KL LLL) _)) ∙ + ( ap + ( map-inv-is-equiv (KL LLL)) + ( ( left-precomp-associative-comul-density-comonad-Precategory) ∙ + ( inv right-precomp-associative-comul-density-comonad-Precategory))) ∙ + ( is-retraction-map-inv-is-equiv (KL LLL) _) +``` + +## Definition + +```agda +module _ + {l1 l2 l3 l4 : Level} + (C : Precategory l1 l2) (D : Precategory l3 l4) + (F : functor-Precategory C D) + (Lk : left-kan-extension-Precategory C D D F F) + where + + density-comonad-Precategory : comonad-Precategory D + density-comonad-Precategory = + ( extension-left-kan-extension-Precategory C D D F F Lk , + counit-density-comonad-Precategory C D F Lk) , + ( comul-density-comonad-Precategory C D F Lk) , + ( ( associative-comul-density-comonad-Precategory C D F Lk) , + ( ( left-counit-law-comul-density-comonad-Precategory C D F Lk) , + ( right-counit-law-comul-density-comonad-Precategory C D F Lk))) +``` + +## See also + +- [Codensity monad](codensity-monads-on-precategories.md) for the dual concept diff --git a/src/category-theory/left-extensions-precategories.lagda.md b/src/category-theory/left-extensions-precategories.lagda.md index 0df357b7f0..915012c6e5 100644 --- a/src/category-theory/left-extensions-precategories.lagda.md +++ b/src/category-theory/left-extensions-precategories.lagda.md @@ -279,7 +279,7 @@ module _ pr2 (square-left-extension-Precategory L) = comp-natural-transformation-Precategory C D ( F) - (comp-functor-Precategory C D D + ( comp-functor-Precategory C D D ( extension-left-extension-Precategory C D D F F L) ( F)) ( comp-functor-Precategory C D D @@ -289,7 +289,7 @@ module _ ( F)) ( left-whisker-natural-transformation-Precategory C D D ( F) - (comp-functor-Precategory C D D + ( comp-functor-Precategory C D D ( extension-left-extension-Precategory C D D F F L) ( F)) ( extension-left-extension-Precategory C D D F F L) From 3213694b8ff3226a50e0ce900cd2a6cb6766abe9 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 17 Jun 2025 16:07:23 -0400 Subject: [PATCH 13/20] Typos --- .../codensity-monads-on-precategories.lagda.md | 2 +- .../density-comonads-on-precategories.lagda.md | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/category-theory/codensity-monads-on-precategories.lagda.md b/src/category-theory/codensity-monads-on-precategories.lagda.md index 01ae7df622..0e67fbbb9e 100644 --- a/src/category-theory/codensity-monads-on-precategories.lagda.md +++ b/src/category-theory/codensity-monads-on-precategories.lagda.md @@ -598,7 +598,7 @@ module _ ## See also -- [Codensity monad](codensity-monads-on-precategories.md) for the dual concept +- [Density comonads](density-comonads-on-precategories.md) for the dual concept ## External links diff --git a/src/category-theory/density-comonads-on-precategories.lagda.md b/src/category-theory/density-comonads-on-precategories.lagda.md index 526e3d7da1..5b0d34b0a1 100644 --- a/src/category-theory/density-comonads-on-precategories.lagda.md +++ b/src/category-theory/density-comonads-on-precategories.lagda.md @@ -1,4 +1,4 @@ -# Density comonads in precategories +# Density comonads on precategories ```agda module category-theory.density-comonads-on-precategories where @@ -589,4 +589,4 @@ module _ ## See also -- [Codensity monad](codensity-monads-on-precategories.md) for the dual concept +- [Codensity monads](codensity-monads-on-precategories.md) for the dual concept From 3dcb0fd1f5b98ae6d5a89069a193d68bb7e76a93 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Tue, 17 Jun 2025 16:25:40 -0400 Subject: [PATCH 14/20] Link typos --- .../codensity-monads-on-precategories.lagda.md | 11 ++++++----- .../density-comonads-on-precategories.lagda.md | 5 +++-- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/category-theory/codensity-monads-on-precategories.lagda.md b/src/category-theory/codensity-monads-on-precategories.lagda.md index 0e67fbbb9e..f5d3bf801d 100644 --- a/src/category-theory/codensity-monads-on-precategories.lagda.md +++ b/src/category-theory/codensity-monads-on-precategories.lagda.md @@ -27,10 +27,10 @@ open import foundation.universe-levels ## Idea Given an arbitrary [functor](category-theory.functors-precategories.md) -`F : C → D`, any [right Kan -extension](category-theory.right-kan-extensions-precategories.md] `R` of `F` -along itself `F` has a canonical -[monad](category-theory.monads-on-precategories.md] structure, called the +`F : C → D`, any +[right Kan extension](category-theory.right-kan-extensions-precategories.md) `R` +of `F` along itself `F` has a canonical +[monad](category-theory.monads-on-precategories.md) structure, called the {{#concept "codensity monad" Agda=codensity-monad-Precategory WD="codensity monad" WDID=Q97359844}} of `R`. @@ -598,7 +598,8 @@ module _ ## See also -- [Density comonads](density-comonads-on-precategories.md) for the dual concept +- [Density comonads](category-theory.density-comonads-on-precategories.md) for + the dual concept ## External links diff --git a/src/category-theory/density-comonads-on-precategories.lagda.md b/src/category-theory/density-comonads-on-precategories.lagda.md index 5b0d34b0a1..c0a0188013 100644 --- a/src/category-theory/density-comonads-on-precategories.lagda.md +++ b/src/category-theory/density-comonads-on-precategories.lagda.md @@ -30,7 +30,7 @@ Given an arbitrary [functor](category-theory.functors-precategories.md) `F : C → D`, any [left Kan extension](category-theory.left-kan-extensions-precategories.md] `L` of `F` along itself `F` has a canonical -[comonad](category-theory.comonads-on-precategories.md] structure, called the +[comonad](category-theory.comonads-on-precategories.md) structure, called the {{#concept "density comonad" Agda=density-comonad-Precategory}} of `L`. ## Comonad structure @@ -589,4 +589,5 @@ module _ ## See also -- [Codensity monads](codensity-monads-on-precategories.md) for the dual concept +- [Codensity monads](category-theory.codensity-monads-on-precategories.md) for + the dual concept From 29fbcb29cdb53ca1e7d6a05992278426d1c1b924 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Wed, 18 Jun 2025 14:55:31 -0400 Subject: [PATCH 15/20] Remove pullbacks and pushouts --- src/category-theory.lagda.md | 1 - .../pullbacks-in-precategories.lagda.md | 16 +- .../pushouts-in-precategories.lagda.md | 175 ------------------ 3 files changed, 6 insertions(+), 186 deletions(-) delete mode 100644 src/category-theory/pushouts-in-precategories.lagda.md diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index 5d61fc3b57..666657e071 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -161,7 +161,6 @@ open import category-theory.products-in-precategories public open import category-theory.products-of-precategories public open import category-theory.pseudomonic-functors-precategories public open import category-theory.pullbacks-in-precategories public -open import category-theory.pushouts-in-precategories public open import category-theory.replete-subprecategories public open import category-theory.representable-functors-categories public open import category-theory.representable-functors-large-precategories public diff --git a/src/category-theory/pullbacks-in-precategories.lagda.md b/src/category-theory/pullbacks-in-precategories.lagda.md index 4028c54a62..aaefb61ec6 100644 --- a/src/category-theory/pullbacks-in-precategories.lagda.md +++ b/src/category-theory/pullbacks-in-precategories.lagda.md @@ -106,10 +106,10 @@ module _ hom-Precategory C object-pullback-obj-Precategory z pr2-pullback-obj-Precategory = pr1 (pr2 (pr2 (t x y z f g))) - comm-pullback-obj-Precategory : + pullback-square-Precategory-comm : comp-hom-Precategory C f pr1-pullback-obj-Precategory ＝ comp-hom-Precategory C g pr2-pullback-obj-Precategory - comm-pullback-obj-Precategory = pr1 (pr2 (pr2 (pr2 (t x y z f g)))) + pullback-square-Precategory-comm = pr1 (pr2 (pr2 (pr2 (t x y z f g)))) module _ (w' : obj-Precategory C) @@ -123,20 +123,20 @@ module _ morphism-into-pullback-obj-Precategory = pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)) - comm-morphism-into-pr1-pullback-obj-Precategory : + morphism-into-pullback-comm-pr1 : comp-hom-Precategory C pr1-pullback-obj-Precategory morphism-into-pullback-obj-Precategory ＝ p₁' - comm-morphism-into-pr1-pullback-obj-Precategory = + morphism-into-pullback-comm-pr1 = pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) - comm-morphism-into-pr2-pullback-obj-Precategory : + morphism-into-pullback-comm-pr2 : comp-hom-Precategory C pr2-pullback-obj-Precategory morphism-into-pullback-obj-Precategory ＝ p₂' - comm-morphism-into-pr2-pullback-obj-Precategory = + morphism-into-pullback-comm-pr2 = pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))) is-unique-morphism-into-pullback-obj-Precategory : @@ -172,7 +172,3 @@ module _ pr2 is-pullback-prop-Precategory = is-prop-is-pullback-obj-Precategory ``` - -## See also - -- [Pushouts](category-theory.pushouts-in-precategories.md) for the dual concept. diff --git a/src/category-theory/pushouts-in-precategories.lagda.md b/src/category-theory/pushouts-in-precategories.lagda.md deleted file mode 100644 index d3f874da9b..0000000000 --- a/src/category-theory/pushouts-in-precategories.lagda.md +++ /dev/null @@ -1,175 +0,0 @@ -# Pushouts in precategories - -```agda -module category-theory.pushouts-in-precategories where -``` - -
Imports - -```agda -open import category-theory.opposite-precategories -open import category-theory.precategories -open import category-theory.pullbacks-in-precategories - -open import foundation.action-on-identifications-functions -open import foundation.cartesian-product-types -open import foundation.contractible-types -open import foundation.dependent-pair-types -open import foundation.identity-types -open import foundation.iterated-dependent-product-types -open import foundation.propositions -open import foundation.uniqueness-quantification -open import foundation.universe-levels -``` - -
- -## Idea - -A -{{#concept "pushout" Disambiguation="of objects in precategories" Agda=pushout-obj-Precategory}} -of two morphisms `f : hom x y` and `g : hom x z` in a category `C` consists of: - -- an object `w` -- morphisms `i₁ : hom y w` and `i₂ : hom z w` such that -- `i₁ ∘ f = i₂ ∘ g` together with the universal property that for every - object`w'` and pair of morphisms `i₁' : hom y w'` and `i₂' : hom z w'` such - that `i₁' ∘ f = i₂' ∘ g` there exists a unique morphism `h : hom w w'` such - that -- `h ∘ i₁ = i₁'` -- `h ∘ i₂ = i₂'`. - -We say that `C` -{{#concept "has all pushouts" Disambiguation="precategory" Agda=has-all-pushout-obj-Precategory}} -if there is a choice of a pushout for each object `x` and pair of morphisms out -of `x` in `C`. - -All definitions here are defined in terms of pullbacks in the -[opposite precategory](category-theory.opposite-precategories.md); see -[pullbacks](category-theory.pullbacks-in-precategories.md) for details. - -## Definition - -```agda -module _ - {l1 l2 : Level} (C : Precategory l1 l2) - where - - is-pushout-obj-Precategory : - (x y z : obj-Precategory C) → - (f : hom-Precategory C x y) → - (g : hom-Precategory C x z) → - (w : obj-Precategory C) → - (i₁ : hom-Precategory C y w) → - (i₂ : hom-Precategory C z w) → - comp-hom-Precategory C i₁ f ＝ comp-hom-Precategory C i₂ g → - UU (l1 ⊔ l2) - is-pushout-obj-Precategory = - is-pullback-obj-Precategory (opposite-Precategory C) - - pushout-obj-Precategory : - (x y z : obj-Precategory C) → - hom-Precategory C x y → - hom-Precategory C x z → - UU (l1 ⊔ l2) - pushout-obj-Precategory = - pullback-obj-Precategory (opposite-Precategory C) - - has-all-pushout-obj-Precategory : UU (l1 ⊔ l2) - has-all-pushout-obj-Precategory = - has-all-pullback-obj-Precategory (opposite-Precategory C) - -module _ - {l1 l2 : Level} (C : Precategory l1 l2) - (t : has-all-pushout-obj-Precategory C) - (x y z : obj-Precategory C) - (f : hom-Precategory C x y) - (g : hom-Precategory C x z) - where - - object-pushout-obj-Precategory : obj-Precategory C - object-pushout-obj-Precategory = - object-pullback-obj-Precategory (opposite-Precategory C) t x y z f g - - inl-pushout-obj-Precategory : - hom-Precategory C y object-pushout-obj-Precategory - inl-pushout-obj-Precategory = - pr1-pullback-obj-Precategory (opposite-Precategory C) t x y z f g - - inr-pushout-obj-Precategory : - hom-Precategory C z object-pushout-obj-Precategory - inr-pushout-obj-Precategory = - pr2-pullback-obj-Precategory (opposite-Precategory C) t x y z f g - - comm-pushout-obj-Precategory : - comp-hom-Precategory C inl-pushout-obj-Precategory f ＝ - comp-hom-Precategory C inr-pushout-obj-Precategory g - comm-pushout-obj-Precategory = - comm-pullback-obj-Precategory (opposite-Precategory C) t x y z f g - - module _ - (w' : obj-Precategory C) - (i₁' : hom-Precategory C y w') - (i₂' : hom-Precategory C z w') - (α : comp-hom-Precategory C i₁' f ＝ comp-hom-Precategory C i₂' g) - where - - morphism-from-pushout-obj-Precategory : - hom-Precategory C object-pushout-obj-Precategory w' - morphism-from-pushout-obj-Precategory = - morphism-into-pullback-obj-Precategory (opposite-Precategory C) - t x y z f g w' i₁' i₂' α - - comm-morphism-from-inl-pushout-obj-Precategory : - comp-hom-Precategory C - morphism-from-pushout-obj-Precategory - inl-pushout-obj-Precategory ＝ - i₁' - comm-morphism-from-inl-pushout-obj-Precategory = - comm-morphism-into-pr1-pullback-obj-Precategory (opposite-Precategory C) - t x y z f g w' i₁' i₂' α - - comm-morphism-from-inr-pushout-obj-Precategory : - comp-hom-Precategory C - morphism-from-pushout-obj-Precategory - inr-pushout-obj-Precategory ＝ - i₂' - comm-morphism-from-inr-pushout-obj-Precategory = - comm-morphism-into-pr2-pullback-obj-Precategory (opposite-Precategory C) - t x y z f g w' i₁' i₂' α - - is-unique-morphism-from-pushout-obj-Precategory : - (h' : hom-Precategory C object-pushout-obj-Precategory w') → - comp-hom-Precategory C h' inl-pushout-obj-Precategory ＝ i₁' → - comp-hom-Precategory C h' inr-pushout-obj-Precategory ＝ i₂' → - morphism-from-pushout-obj-Precategory ＝ h' - is-unique-morphism-from-pushout-obj-Precategory = - is-unique-morphism-into-pullback-obj-Precategory (opposite-Precategory C) - t x y z f g w' i₁' i₂' α - -module _ - {l1 l2 : Level} (C : Precategory l1 l2) - (x y z : obj-Precategory C) - (f : hom-Precategory C x y) - (g : hom-Precategory C x z) - (w : obj-Precategory C) - (i₁ : hom-Precategory C y w) - (i₂ : hom-Precategory C z w) - (α : comp-hom-Precategory C i₁ f ＝ comp-hom-Precategory C i₂ g) - where - - is-prop-is-pushout-obj-Precategory : - is-prop (is-pushout-obj-Precategory C x y z f g w i₁ i₂ α) - is-prop-is-pushout-obj-Precategory = - is-prop-is-pullback-obj-Precategory (opposite-Precategory C) - x y z f g w i₁ i₂ α - - is-pushout-prop-Precategory : Prop (l1 ⊔ l2) - is-pushout-prop-Precategory = - is-pullback-prop-Precategory (opposite-Precategory C) x y z f g w i₁ i₂ α -``` - -## See also - -- [Pullbacks](category-theory.pullbacks-in-precategories.md) for the dual - concept. From 28cfe79881d1609234731deb0e435fa8cfda0839 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Wed, 18 Jun 2025 15:00:34 -0400 Subject: [PATCH 16/20] Typo; rename coherence of (co)monad (co)algebras --- .../left-extensions-precategories.lagda.md | 2 +- ...hisms-algebras-monads-on-precategories.lagda.md | 8 ++++---- ...s-coalgebras-comonads-on-precategories.lagda.md | 14 +++++++------- ...ry-of-algebras-monads-on-precategories.lagda.md | 2 +- ...f-coalgebras-comonads-on-precategories.lagda.md | 2 +- .../right-extensions-precategories.lagda.md | 2 +- 6 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/category-theory/left-extensions-precategories.lagda.md b/src/category-theory/left-extensions-precategories.lagda.md index 915012c6e5..b12723075d 100644 --- a/src/category-theory/left-extensions-precategories.lagda.md +++ b/src/category-theory/left-extensions-precategories.lagda.md @@ -154,7 +154,7 @@ module _ ## Properties -### Characterization of equality left extensions of functors between precategories +### Characterization of equality between left extensions of functors between precategories ```agda coherence-htpy-left-extension-Precategory : diff --git a/src/category-theory/morphisms-algebras-monads-on-precategories.lagda.md b/src/category-theory/morphisms-algebras-monads-on-precategories.lagda.md index 670e99fddf..6007b07449 100644 --- a/src/category-theory/morphisms-algebras-monads-on-precategories.lagda.md +++ b/src/category-theory/morphisms-algebras-monads-on-precategories.lagda.md @@ -77,7 +77,7 @@ module _ hom-endofunctor-monad-Precategory C T ( hom-morphism-algebra-monad-Precategory f g h) - comm-hom-morphism-algebra-monad-Precategory : + coh-hom-morphism-algebra-monad-Precategory : (f g : algebra-monad-Precategory C T) (h : morphism-algebra-monad-Precategory f g) → coherence-square-hom-Precategory C @@ -85,7 +85,7 @@ module _ ( hom-algebra-monad-Precategory C T f) ( hom-algebra-monad-Precategory C T g) ( hom-morphism-algebra-monad-Precategory f g h) - comm-hom-morphism-algebra-monad-Precategory f g h = pr2 h + coh-hom-morphism-algebra-monad-Precategory f g h = pr2 h comp-morphism-algebra-monad-Precategory : (a b c : algebra-monad-Precategory C T) @@ -104,8 +104,8 @@ module _ ( hom-algebra-monad-Precategory C T c) ( hom-morphism-algebra-monad-Precategory a b f) ( hom-morphism-algebra-monad-Precategory b c g) - ( comm-hom-morphism-algebra-monad-Precategory a b f) - ( comm-hom-morphism-algebra-monad-Precategory b c g)) ∙ + ( coh-hom-morphism-algebra-monad-Precategory a b f) + ( coh-hom-morphism-algebra-monad-Precategory b c g)) ∙ ( ap ( postcomp-hom-Precategory C (hom-algebra-monad-Precategory C T c) _) ( inv (preserves-comp-endofunctor-monad-Precategory C T _ _))) diff --git a/src/category-theory/morphisms-coalgebras-comonads-on-precategories.lagda.md b/src/category-theory/morphisms-coalgebras-comonads-on-precategories.lagda.md index 5b8586a57f..9ec4962488 100644 --- a/src/category-theory/morphisms-coalgebras-comonads-on-precategories.lagda.md +++ b/src/category-theory/morphisms-coalgebras-comonads-on-precategories.lagda.md @@ -78,7 +78,7 @@ module _ hom-endofunctor-comonad-Precategory C T ( hom-morphism-coalgebra-comonad-Precategory f g h) - comm-hom-morphism-coalgebra-comonad-Precategory : + coh-hom-morphism-coalgebra-comonad-Precategory : (f g : coalgebra-comonad-Precategory C T) (h : morphism-coalgebra-comonad-Precategory f g) → coherence-square-hom-Precategory C @@ -86,7 +86,7 @@ module _ ( hom-coalgebra-comonad-Precategory C T f) ( hom-coalgebra-comonad-Precategory C T g) ( bottom-hom-morphism-coalgebra-comonad-Precategory f g h) - comm-hom-morphism-coalgebra-comonad-Precategory f g h = pr2 h + coh-hom-morphism-coalgebra-comonad-Precategory f g h = pr2 h comp-morphism-coalgebra-comonad-Precategory : (a b c : coalgebra-comonad-Precategory C T) @@ -97,9 +97,9 @@ module _ ( comp-hom-Precategory C ( hom-morphism-coalgebra-comonad-Precategory b c g) ( hom-morphism-coalgebra-comonad-Precategory a b f)) , - (ap - (precomp-hom-Precategory C (hom-coalgebra-comonad-Precategory C T a) _) - (preserves-comp-endofunctor-comonad-Precategory C T _ _)) ∙ + ( ap + ( precomp-hom-Precategory C (hom-coalgebra-comonad-Precategory C T a) _) + ( preserves-comp-endofunctor-comonad-Precategory C T _ _)) ∙ ( pasting-horizontal-coherence-square-hom-Precategory C ( hom-morphism-coalgebra-comonad-Precategory a b f) ( hom-morphism-coalgebra-comonad-Precategory b c g) @@ -108,8 +108,8 @@ module _ ( hom-coalgebra-comonad-Precategory C T c) ( bottom-hom-morphism-coalgebra-comonad-Precategory a b f) ( bottom-hom-morphism-coalgebra-comonad-Precategory b c g) - ( comm-hom-morphism-coalgebra-comonad-Precategory a b f) - ( comm-hom-morphism-coalgebra-comonad-Precategory b c g)) + ( coh-hom-morphism-coalgebra-comonad-Precategory a b f) + ( coh-hom-morphism-coalgebra-comonad-Precategory b c g)) is-set-morphism-coalgebra-comonad-Precategory : (f g : coalgebra-comonad-Precategory C T) → diff --git a/src/category-theory/precategory-of-algebras-monads-on-precategories.lagda.md b/src/category-theory/precategory-of-algebras-monads-on-precategories.lagda.md index bd8572ad93..58de97bfc9 100644 --- a/src/category-theory/precategory-of-algebras-monads-on-precategories.lagda.md +++ b/src/category-theory/precategory-of-algebras-monads-on-precategories.lagda.md @@ -311,7 +311,7 @@ The counit is the vertical map given by the structure map of the algebra ( inv (mul-law-algebra-monad-Precategory C T x))) , ( λ {x} {y} f → eq-pair-Σ - ( comm-hom-morphism-algebra-monad-Precategory C T x y f) + ( coh-hom-morphism-algebra-monad-Precategory C T x y f) ( eq-is-prop (is-set-hom-Precategory C _ _ _ _))) left-triangle-algebras-monad-Precategory : diff --git a/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md b/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md index 6278cc21be..254ce3116b 100644 --- a/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md +++ b/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md @@ -312,7 +312,7 @@ The unit is the horizontal map given by the structure map of the coalgebra ( comul-law-coalgebra-comonad-Precategory C T x)) , ( λ {x} {y} f → eq-pair-Σ - ( comm-hom-morphism-coalgebra-comonad-Precategory C T x y f) + ( coh-hom-morphism-coalgebra-comonad-Precategory C T x y f) ( eq-is-prop (is-set-hom-Precategory C _ _ _ _))) right-triangle-coalgebras-comonad-Precategory : diff --git a/src/category-theory/right-extensions-precategories.lagda.md b/src/category-theory/right-extensions-precategories.lagda.md index f5469c68d3..3a50299151 100644 --- a/src/category-theory/right-extensions-precategories.lagda.md +++ b/src/category-theory/right-extensions-precategories.lagda.md @@ -154,7 +154,7 @@ module _ ## Properties -### Characterization of equality right extensions of functors between precategories +### Characterization of equality between right extensions of functors between precategories ```agda coherence-htpy-right-extension-Precategory : From 1f7350d29ddb2239157bfad2b2ed00aade8eff9e Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Thu, 19 Jun 2025 23:51:33 -0400 Subject: [PATCH 17/20] Apply suggestions from code review --- .../cocones-precategories.lagda.md | 32 +++++++++++-------- ...codensity-monads-on-precategories.lagda.md | 2 +- .../cones-precategories.lagda.md | 26 ++++++++------- ...density-comonads-on-precategories.lagda.md | 2 +- 4 files changed, 36 insertions(+), 26 deletions(-) diff --git a/src/category-theory/cocones-precategories.lagda.md b/src/category-theory/cocones-precategories.lagda.md index e1ef57e5f8..b83398bd9c 100644 --- a/src/category-theory/cocones-precategories.lagda.md +++ b/src/category-theory/cocones-precategories.lagda.md @@ -51,9 +51,10 @@ open import foundation.universe-levels A {{#concept "cocone" Disambiguation="under a functor between precategories" Agda=cocone-Precategory}} under a [functor](category-theory.functors-precategories.md) `F` between -[precategories](category-theory.precategories.md) is a +[precategories](category-theory.precategories.md) is an object `d` of the +codomain together with a [natural transformation](category-theory.natural-transformations-functors-precategories.md) -from a [constant functor](category-theory.constant-functors.md) to `F`. +from `F` to the [constant functor](category-theory.constant-functors.md) at `d`. In this context, we usually think of (and refer to) the functor `F` as a **diagram** in its codomain, A cocone under such diagram then corresponds to an @@ -174,7 +175,7 @@ module _ ## Properties -### Characterization of equality of cocones over functors between precategories +### Characterization of equality of cocones ```agda coherence-htpy-cocone-Precategory : @@ -268,33 +269,38 @@ module _ equiv-left-extension-cocone-Precategory : cocone-Precategory ≃ left-extension-Precategory C terminal-Precategory D - (terminal-functor-Precategory C) F + ( terminal-functor-Precategory C) + ( F) equiv-left-extension-cocone-Precategory = equiv-Σ-equiv-base - ( λ K → natural-transformation-Precategory C D - ( F) - ( comp-functor-Precategory C terminal-Precategory D - ( K) - ( terminal-functor-Precategory C))) - ( equiv-point-Precategory D) + ( λ K → + natural-transformation-Precategory C D + ( F) + ( comp-functor-Precategory C terminal-Precategory D + ( K) + ( terminal-functor-Precategory C))) + ( equiv-point-Precategory D) left-extension-cocone-Precategory : cocone-Precategory → left-extension-Precategory C terminal-Precategory D - (terminal-functor-Precategory C) F + ( terminal-functor-Precategory C) + ( F) left-extension-cocone-Precategory = map-equiv equiv-left-extension-cocone-Precategory cocone-left-extension-Precategory : left-extension-Precategory C terminal-Precategory D - (terminal-functor-Precategory C) F → + ( terminal-functor-Precategory C) + ( F) → cocone-Precategory cocone-left-extension-Precategory = map-inv-equiv equiv-left-extension-cocone-Precategory vertex-left-extension-Precategory : left-extension-Precategory C terminal-Precategory D - (terminal-functor-Precategory C) F → + ( terminal-functor-Precategory C) + ( F) → obj-Precategory D vertex-left-extension-Precategory R = vertex-cocone-Precategory diff --git a/src/category-theory/codensity-monads-on-precategories.lagda.md b/src/category-theory/codensity-monads-on-precategories.lagda.md index f5d3bf801d..a7d450b959 100644 --- a/src/category-theory/codensity-monads-on-precategories.lagda.md +++ b/src/category-theory/codensity-monads-on-precategories.lagda.md @@ -29,7 +29,7 @@ open import foundation.universe-levels Given an arbitrary [functor](category-theory.functors-precategories.md) `F : C → D`, any [right Kan extension](category-theory.right-kan-extensions-precategories.md) `R` -of `F` along itself `F` has a canonical +of `F` along itself has a canonical [monad](category-theory.monads-on-precategories.md) structure, called the {{#concept "codensity monad" Agda=codensity-monad-Precategory WD="codensity monad" WDID=Q97359844}} of `R`. diff --git a/src/category-theory/cones-precategories.lagda.md b/src/category-theory/cones-precategories.lagda.md index b041ffe0da..5d796954a5 100644 --- a/src/category-theory/cones-precategories.lagda.md +++ b/src/category-theory/cones-precategories.lagda.md @@ -51,9 +51,10 @@ open import foundation.universe-levels A {{#concept "cone" Disambiguation="over a functor between precategories" Agda=cone-Precategory}} over a [functor](category-theory.functors-precategories.md) `F` between -[precategories](category-theory.precategories.md) is a +[precategories](category-theory.precategories.md) is an object `d` of the +codomain together with a [natural transformation](category-theory.natural-transformations-functors-precategories.md) -from a [constant functor](category-theory.constant-functors.md) to `F`. +from the [constant functor](category-theory.constant-functors.md) at `d` to `F`. In this context, we usually think of (and refer to) the functor `F` as a **diagram** in its codomain, A cone over such diagram then corresponds to an @@ -175,7 +176,7 @@ module _ ## Properties -### Characterization of equality of cones over functors between precategories +### Characterization of equality of cones ```agda coherence-htpy-cone-Precategory : @@ -267,15 +268,17 @@ module _ equiv-right-extension-cone-Precategory : cone-Precategory ≃ right-extension-Precategory C terminal-Precategory D - (terminal-functor-Precategory C) F + ( terminal-functor-Precategory C) + ( F) equiv-right-extension-cone-Precategory = equiv-Σ-equiv-base - ( λ K → natural-transformation-Precategory C D - ( comp-functor-Precategory C terminal-Precategory D - ( K) - ( terminal-functor-Precategory C)) - ( F)) - ( equiv-point-Precategory D) + ( λ K → + natural-transformation-Precategory C D + ( comp-functor-Precategory C terminal-Precategory D + ( K) + ( terminal-functor-Precategory C)) + ( F)) + ( equiv-point-Precategory D) right-extension-cone-Precategory : cone-Precategory → @@ -293,7 +296,8 @@ module _ vertex-right-extension-Precategory : right-extension-Precategory C terminal-Precategory D - (terminal-functor-Precategory C) F → + ( terminal-functor-Precategory C) + ( F) → obj-Precategory D vertex-right-extension-Precategory R = vertex-cone-Precategory diff --git a/src/category-theory/density-comonads-on-precategories.lagda.md b/src/category-theory/density-comonads-on-precategories.lagda.md index c0a0188013..66e94ddc78 100644 --- a/src/category-theory/density-comonads-on-precategories.lagda.md +++ b/src/category-theory/density-comonads-on-precategories.lagda.md @@ -29,7 +29,7 @@ open import foundation.universe-levels Given an arbitrary [functor](category-theory.functors-precategories.md) `F : C → D`, any [left Kan extension](category-theory.left-kan-extensions-precategories.md] `L` of `F` -along itself `F` has a canonical +along itself has a canonical [comonad](category-theory.comonads-on-precategories.md) structure, called the {{#concept "density comonad" Agda=density-comonad-Precategory}} of `L`. From 5a99ffccd5cd75e54c39617b6775811b0e6b2879 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Fri, 20 Jun 2025 11:09:44 -0400 Subject: [PATCH 18/20] Add "See also" --- src/category-theory/cocones-precategories.lagda.md | 5 +++++ src/category-theory/colimits-precategories.lagda.md | 4 ++++ src/category-theory/cones-precategories.lagda.md | 5 +++++ src/category-theory/limits-precategories.lagda.md | 4 ++++ 4 files changed, 18 insertions(+) diff --git a/src/category-theory/cocones-precategories.lagda.md b/src/category-theory/cocones-precategories.lagda.md index b83398bd9c..866974106e 100644 --- a/src/category-theory/cocones-precategories.lagda.md +++ b/src/category-theory/cocones-precategories.lagda.md @@ -306,3 +306,8 @@ module _ vertex-cocone-Precategory ( cocone-left-extension-Precategory R) ``` + +## See also + +- [Colimits](category-theory.colimits-precategories.md) for universal cocones. +- [Cones](category-theory.cones-precategories.md) for the dual concept. diff --git a/src/category-theory/colimits-precategories.lagda.md b/src/category-theory/colimits-precategories.lagda.md index 8d9f1319f9..84be550836 100644 --- a/src/category-theory/colimits-precategories.lagda.md +++ b/src/category-theory/colimits-precategories.lagda.md @@ -273,3 +273,7 @@ module _ colimit'-colimit-Precategory = map-inv-equiv equiv-colimit-colimit'-Precategory ``` + +## See also + +- [Limits](category-theory.limits-precategories.md) for the dual concept. diff --git a/src/category-theory/cones-precategories.lagda.md b/src/category-theory/cones-precategories.lagda.md index 5d796954a5..17de287f12 100644 --- a/src/category-theory/cones-precategories.lagda.md +++ b/src/category-theory/cones-precategories.lagda.md @@ -303,3 +303,8 @@ module _ vertex-cone-Precategory ( cone-right-extension-Precategory R) ``` + +## See also + +- [Limits](category-theory.limits-precategories.md) for universal cones. +- [Cocones](category-theory.cocones-precategories.md) for the dual concept. diff --git a/src/category-theory/limits-precategories.lagda.md b/src/category-theory/limits-precategories.lagda.md index 9ba2e995ab..b648d6ce71 100644 --- a/src/category-theory/limits-precategories.lagda.md +++ b/src/category-theory/limits-precategories.lagda.md @@ -276,3 +276,7 @@ module _ limit'-limit-Precategory = map-inv-equiv equiv-limit-limit'-Precategory ``` + +## See also + +- [Colimits](category-theory.colimits-precategories.md) for the dual concept. From b5dc5ba8edc789e444c4c0e85a91a71805bb868f Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Sat, 21 Jun 2025 10:43:36 -0400 Subject: [PATCH 19/20] Fixes from code review --- .../cocones-precategories.lagda.md | 2 +- ...codensity-monads-on-precategories.lagda.md | 16 +++++----- ...density-comonads-on-precategories.lagda.md | 30 ++----------------- 3 files changed, 13 insertions(+), 35 deletions(-) diff --git a/src/category-theory/cocones-precategories.lagda.md b/src/category-theory/cocones-precategories.lagda.md index 866974106e..34ecdae25f 100644 --- a/src/category-theory/cocones-precategories.lagda.md +++ b/src/category-theory/cocones-precategories.lagda.md @@ -59,7 +59,7 @@ from `F` to the [constant functor](category-theory.constant-functors.md) at `d`. In this context, we usually think of (and refer to) the functor `F` as a **diagram** in its codomain, A cocone under such diagram then corresponds to an element `d`, called the **vertex** of the cocone, equipped with components -`d → F x` satisfying the naturality condition. +`F x → d` satisfying the naturality condition. For example, if `F` corresponds to the diagram `F x → F y`, then a cocone under `F` corresponds to a commuting triangle as below. diff --git a/src/category-theory/codensity-monads-on-precategories.lagda.md b/src/category-theory/codensity-monads-on-precategories.lagda.md index a7d450b959..136955ceff 100644 --- a/src/category-theory/codensity-monads-on-precategories.lagda.md +++ b/src/category-theory/codensity-monads-on-precategories.lagda.md @@ -46,7 +46,7 @@ definition via the universal property, we have two computation rules for these natural transformations (where ∙ is whiskering): 1. `α ∘ (η ∙ F) ＝ id_F`; and -2. `α ∘ (μ ∙ F) = α ∘ (R ∙ α)`. +2. `α ∘ (μ ∙ F) ＝ α ∘ (R ∙ α)`. ```agda module _ @@ -123,8 +123,8 @@ For the left unit law, if `α : R∘F ⇒ F` is the right Kan extension natural transformation, we show that the composite ```text - (Rμ)F μF α - R∘F ⇒ R²∘F ⇒ R∘F ⇒ R + (Rη)F μF α + R∘F ═════> R²∘F ══> R∘F ═> R ``` is equal to `α`; by uniqueness, `μF ∘ RμF = id`. @@ -237,10 +237,12 @@ module _ The right unit law is similar; we show that the composite is `α` via: ```text - ηRF μF α - RF ⇒ R²F ⇒ RF ⇒ F - α ⇓ Rα ⇓ ∥ - F ⇒ RF ⇒ F + ηRF μF α + RF ═══> R²F ══>RF ══> F + ║ ║ ║ + α ║ Rα ║ ║ + ∨ ∨ ║ + F ════> RF ═════════> F ηF α ``` diff --git a/src/category-theory/density-comonads-on-precategories.lagda.md b/src/category-theory/density-comonads-on-precategories.lagda.md index 66e94ddc78..03e02fe6ef 100644 --- a/src/category-theory/density-comonads-on-precategories.lagda.md +++ b/src/category-theory/density-comonads-on-precategories.lagda.md @@ -114,20 +114,12 @@ module _ ## Comonad laws -Comonad laws follow from the "uniqueness" part of the right Kan extension. +Comonad laws follow from the "uniqueness" part of the right Kan extension. See +[codensity monads](category-theory.codensity-monads-on-precategories.md) for an +explanation of the (dual) proofs. ### Left counit law -For the left counit law, if `α : L∘F ⇒ F` is the right Kan extension natural -transformation, we show that the composite - -```text - (Lμ)F μF α - L∘F ⇒ L²∘F ⇒ L∘F ⇒ L -``` - -is equal to `α`; by uniqueness, `μF ∘ LμF = id`. - ```agda module _ {l1 l2 l3 l4 : Level} @@ -239,20 +231,6 @@ module _ ### Right counit law -The right counit law is similar; we show that the composite is `α` via: - -```text - ηLF μF α - LF ⇒ L²F ⇒ LF ⇒ F - α ⇓ Lα ⇓ ∥ - F ⇒ LF ⇒ F - ηF α -``` - -The right square (triangle) commutes by "uniqueness" of the right Kan UP; the -left square commutes by naturality of `η`. The bottom composite is then `id` by -the UP again. - ```agda module _ {l1 l2 l3 l4 : Level} @@ -344,8 +322,6 @@ module _ ### Comultiplication is associative -Showing that comultiplication is associative is similar but longer. - ```agda module _ {l1 l2 l3 l4 : Level} From 425e4b147d1fee34171b8536622ed019340fd834 Mon Sep 17 00:00:00 2001 From: Ben Connors Date: Sat, 21 Jun 2025 11:37:30 -0400 Subject: [PATCH 20/20] Apply suggestions from code review Co-authored-by: Fredrik Bakke --- .../codensity-monads-on-precategories.lagda.md | 10 +++++----- .../density-comonads-on-precategories.lagda.md | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/category-theory/codensity-monads-on-precategories.lagda.md b/src/category-theory/codensity-monads-on-precategories.lagda.md index 136955ceff..83a93d2b72 100644 --- a/src/category-theory/codensity-monads-on-precategories.lagda.md +++ b/src/category-theory/codensity-monads-on-precategories.lagda.md @@ -238,11 +238,11 @@ The right unit law is similar; we show that the composite is `α` via: ```text ηRF μF α - RF ═══> R²F ══>RF ══> F - ║ ║ ║ - α ║ Rα ║ ║ - ∨ ∨ ║ - F ════> RF ═════════> F + RF ═══> R²F ══> RF ══> F + ║ ║ ║ + α ║ Rα ║ ║ + ∨ ∨ ║ + F ════> RF ══════════> F ηF α ``` diff --git a/src/category-theory/density-comonads-on-precategories.lagda.md b/src/category-theory/density-comonads-on-precategories.lagda.md index 03e02fe6ef..711e496315 100644 --- a/src/category-theory/density-comonads-on-precategories.lagda.md +++ b/src/category-theory/density-comonads-on-precategories.lagda.md @@ -45,7 +45,7 @@ definition via the universal property, we have two computation rules for these natural transformations (where ∙ is whiskering): 1. `α ∘ (η ∙ F) ＝ id_F`; and -2. `α ∘ (μ ∙ F) = α ∘ (L ∙ α)`. +2. `α ∘ (μ ∙ F) ＝ α ∘ (L ∙ α)`. ```agda module _