Dualize limits, right Kan extensions, and monads

src/category-theory.lagda.md

@@ -25,22 +25,28 @@ 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.cocones-precategories public
 open import category-theory.codensity-monads-on-precategories public
+open import category-theory.colimits-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
 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
@@ -102,6 +108,8 @@ open import category-theory.large-function-precategories public
 open import category-theory.large-precategories public
 open import category-theory.large-subcategories public
 open import category-theory.large-subprecategories public
+open import category-theory.left-extensions-precategories public
+open import category-theory.left-kan-extensions-precategories public
 open import category-theory.limits-precategories public
 open import category-theory.maps-categories public
 open import category-theory.maps-from-small-to-large-categories public
@@ -112,6 +120,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
@@ -138,6 +147,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
@@ -151,6 +161,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

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))
 ```

src/category-theory/coalgebras-comonads-on-precategories.lagda.md

@@ -0,0 +1,103 @@
+# Coalgebras over comonads on precategories
+
+```agda
+module category-theory.coalgebras-comonads-on-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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)
+  {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
+
+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 C T 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 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 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 C T
+      ( hom-coalgebra-comonad-Precategory f)
+  comul-law-coalgebra-comonad-Precategory f = pr2 (pr2 (pr2 f))
+```