diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md
index ad5056634c..666657e071 100644
--- a/src/category-theory.lagda.md
+++ b/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
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
new file mode 100644
index 0000000000..a17d025399
--- /dev/null
+++ b/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))
+```
diff --git a/src/category-theory/cocones-precategories.lagda.md b/src/category-theory/cocones-precategories.lagda.md
new file mode 100644
index 0000000000..34ecdae25f
--- /dev/null
+++ b/src/category-theory/cocones-precategories.lagda.md
@@ -0,0 +1,313 @@
+# Cocones in precategories
+
+```agda
+module category-theory.cocones-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## Idea
+
+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 an object `d` of the
+codomain together with a
+[natural transformation](category-theory.natural-transformations-functors-precategories.md)
+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
+`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.
+
+```text
+ Fx ----> Fy
+   \     /
+    \   /
+     ∨ ∨
+      d
+```
+
+Equivalently, we can see a cocone under `F` as a
+[left extension](category-theory.left-extensions-precategories.md) of `F` along
+the terminal functor into the
+[terminal precategory](category-theory.terminal-category.md).
+
+## Definitions
+
+### The type of cocones under 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
+
+```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)
+```
+
+## 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/codensity-monads-on-precategories.lagda.md b/src/category-theory/codensity-monads-on-precategories.lagda.md
index f02e0863b5..83a93d2b72 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 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`.
 
@@ -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`.
@@ -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))) ∙
@@ -243,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          α
 ```
 
@@ -303,7 +299,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 +389,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 +425,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 +475,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 +543,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 +598,11 @@ module _
         ( right-unit-law-mul-codensity-monad-Precategory C D F Rk)))
 ```
 
+## See also
+
+- [Density comonads](category-theory.density-comonads-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/colimits-precategories.lagda.md b/src/category-theory/colimits-precategories.lagda.md
new file mode 100644
index 0000000000..84be550836
--- /dev/null
+++ b/src/category-theory/colimits-precategories.lagda.md
@@ -0,0 +1,279 @@
+# Colimits in precategories
+
+```agda
+module category-theory.colimits-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+
+open import foundation-core.homotopies
+```
+
+</details>
+
+## 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](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
+`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.
+
+## Definitions
+
+### Colimiting cocones
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} (C : Precategory l1 l2) (D : Precategory l3 l4)
+  (F : functor-Precategory C D)
+  where
+
+  is-colimit-cocone-Precategory :
+    cocone-Precategory C D F → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
+  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-colimit-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-colimit-colimit-Precategory :
+    (τ : colimit-Precategory) →
+    is-colimit-cocone-Precategory (cocone-colimit-Precategory τ)
+  is-colimit-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-colimit-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-colimit-cocone-Precategory :
+    (τ : 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-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-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) τ)
+  equiv-is-left-kan-extension-is-colimit-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 : 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) τ)
+          ( 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))
+              ( _)
+              ( _)
+              ( refl-htpy))
+
+  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-colimit-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
+```
+
+## See also
+
+- [Limits](category-theory.limits-precategories.md) for the dual concept.
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..372923f5fa
--- /dev/null
+++ b/src/category-theory/comonads-on-precategories.lagda.md
@@ -0,0 +1,452 @@
+# Comonads on precategories
+
+```agda
+module category-theory.comonads-on-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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)
+```
+
+## See also
+
+- [Monads](category-theory.monads-on-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 12df81dc10..17de287f12 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
@@ -166,16 +167,16 @@ 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
 
-### 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,9 +296,15 @@ 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
       ( 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/copointed-endofunctors-precategories.lagda.md b/src/category-theory/copointed-endofunctors-precategories.lagda.md
new file mode 100644
index 0000000000..d4845e11f0
--- /dev/null
+++ b/src/category-theory/copointed-endofunctors-precategories.lagda.md
@@ -0,0 +1,147 @@
+# Copointed endofunctors on precategories
+
+```agda
+module category-theory.copointed-endofunctors-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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)
+`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}}
+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)
+```
+
+## See also
+
+- [Pointed endofunctors](category-theory.pointed-endofunctors-precategories.md)
+  for the dual concept.
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..711e496315
--- /dev/null
+++ b/src/category-theory/density-comonads-on-precategories.lagda.md
@@ -0,0 +1,569 @@
+# Density comonads on precategories
+
+```agda
+module category-theory.density-comonads-on-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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 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. See
+[codensity monads](category-theory.codensity-monads-on-precategories.md) for an
+explanation of the (dual) proofs.
+
+### Left counit law
+
+```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
+
+```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
+
+```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 monads](category-theory.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
new file mode 100644
index 0000000000..b12723075d
--- /dev/null
+++ b/src/category-theory/left-extensions-precategories.lagda.md
@@ -0,0 +1,303 @@
+# Left extensions in precategories
+
+```agda
+module category-theory.left-extensions-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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' -----> D
+         G
+```
+
+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
+
+### 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 between 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)
+```
+
+### Self-extensions
+
+In the case of extending a functor along itself, we have distinguished left
+extensions: the identity map gives a left extension (with the identity natural
+transformation) and we can iterate any left extension `L` to get a left
+extension `L²`.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (C : Precategory l1 l2) (D : Precategory l3 l4)
+  (F : functor-Precategory C D)
+  where
+
+  id-left-extension-Precategory : left-extension-Precategory C D D F F
+  pr1 id-left-extension-Precategory = id-functor-Precategory D
+  pr2 id-left-extension-Precategory =
+    id-natural-transformation-Precategory C D F
+
+  square-left-extension-Precategory :
+    (L : left-extension-Precategory C D D F F) →
+    left-extension-Precategory C D D F F
+  pr1 (square-left-extension-Precategory L) =
+    comp-functor-Precategory D D D
+      ( extension-left-extension-Precategory C D D F F L)
+      ( extension-left-extension-Precategory C D D F F L)
+  pr2 (square-left-extension-Precategory L) =
+    comp-natural-transformation-Precategory C D
+      ( F)
+      ( comp-functor-Precategory C D D
+        ( extension-left-extension-Precategory C D D F F L)
+        ( F))
+      ( comp-functor-Precategory C D D
+        ( comp-functor-Precategory D D D
+          ( extension-left-extension-Precategory C D D F F L)
+          ( extension-left-extension-Precategory C D D F F L))
+        ( F))
+      ( left-whisker-natural-transformation-Precategory C D D
+        ( F)
+        ( 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)
+        ( natural-transformation-left-extension-Precategory C D D F F L))
+      ( natural-transformation-left-extension-Precategory C D D F F L)
+```
+
+## 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
new file mode 100644
index 0000000000..70404cd987
--- /dev/null
+++ b/src/category-theory/left-kan-extensions-precategories.lagda.md
@@ -0,0 +1,102 @@
+# Left Kan extensions in precategories
+
+```agda
+module category-theory.left-kan-extensions-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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`. 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.
+
+## 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
+```
+
+## See also
+
+- [Right Kan extensions](category-theory.right-kan-extensions-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 60015d9a58..b648d6ce71 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
 ```
 
 </details>
@@ -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
 
@@ -63,16 +65,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 +87,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 +100,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,18 +155,18 @@ 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-property-is-equiv _
+    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' :
     ( 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
@@ -175,13 +177,14 @@ 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-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 τ =
+    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-limit-Precategory τ =
     equiv-Π _
       ( equiv-point-Precategory D)
       ( λ x →
@@ -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
@@ -239,7 +264,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
@@ -251,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.
diff --git a/src/category-theory/monads-on-precategories.lagda.md b/src/category-theory/monads-on-precategories.lagda.md
index 2cdc8894f6..f0326b232d 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 =
@@ -440,3 +440,7 @@ module _
         ( endofunctor-monad-Precategory)
         ( right-unit-law-mul-monad-Precategory)
 ```
+
+## See also
+
+- [Comonads](category-theory.comonads-on-precategories.md) for the dual concept.
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
new file mode 100644
index 0000000000..9ec4962488
--- /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
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## 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)
+
+  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
+      ( 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)
+  coh-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)
+      ( 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) →
+    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/pointed-endofunctors-precategories.lagda.md b/src/category-theory/pointed-endofunctors-precategories.lagda.md
index 2472a4dab6..eb7d385f9e 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
+
+- [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..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
@@ -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)`.
@@ -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
new file mode 100644
index 0000000000..254ce3116b
--- /dev/null
+++ b/src/category-theory/precategory-of-coalgebras-comonads-on-precategories.lagda.md
@@ -0,0 +1,357 @@
+# The precategory of coalgebras over a comonad
+
+```agda
+module category-theory.precategory-of-coalgebras-comonads-on-precategories where
+```
+
+<details><summary>Imports</summary>
+
+```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
+```
+
+</details>
+
+## Idea
+
+The
+{{#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`.
+
+## 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-Σ
+        ( coh-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))
+```
diff --git a/src/category-theory/right-extensions-precategories.lagda.md b/src/category-theory/right-extensions-precategories.lagda.md
index c36328ce66..3a50299151 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
 
@@ -153,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 :
@@ -295,3 +296,8 @@ module _
         ( extension-right-extension-Precategory C D D F F R)
         ( natural-transformation-right-extension-Precategory C D D F F R))
 ```
+
+## 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 1af7fd92a1..3d9e407cd3 100644
--- a/src/category-theory/right-kan-extensions-precategories.lagda.md
+++ b/src/category-theory/right-kan-extensions-precategories.lagda.md
@@ -28,7 +28,10 @@ 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.
@@ -92,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.
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) →