docs(category_theory/*): the last missing module docs (#14237)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/limits/cones.lean

@@ -8,6 +8,29 @@ import category_theory.discrete_category
 import category_theory.yoneda
 import category_theory.functor.reflects_isomorphisms
 
+/-!
+# Cones and cocones
+
+We define `cone F`, a cone over a functor `F`,
+and `F.cones : Cᵒᵖ ⥤ Type`, the functor associating to `X` the cones over `F` with cone point `X`.
+
+A cone `c` is defined by specifying its cone point `c.X` and a natural transformation `c.π`
+from the constant `c.X` valued functor to `F`.
+
+We provide `c.w f : c.π.app j ≫ F.map f = c.π.app j'` for any `f : j ⟶ j'`
+as a wrapper for `c.π.naturality f` avoiding unneeded identity morphisms.
+
+We define `c.extend f`, where `c : cone F` and `f : Y ⟶ c.X` for some other `Y`,
+which replaces the cone point by `Y` and inserts `f` into each of the components of the cone.
+Similarly we have `c.whisker F` producing a `cone (E ⋙ F)`
+
+We define morphisms of cones, and the category of cones.
+
+We define `cone.postcompose α : cone F ⥤ cone G` for `α` a natural transformation `F ⟶ G`.
+
+And, of course, we dualise all this to cocones as well.
+-/
+
 -- morphism levels before object levels. See note [category_theory universes].
 universes v₁ v₂ v₃ v₄ u₁ u₂ u₃ u₄
 open category_theory

src/category_theory/limits/creates.lean

@@ -5,6 +5,14 @@ Authors: Bhavik Mehta
 -/
 import category_theory.limits.preserves.basic
 
+/-!
+# Creating (co)limits
+
+We say that `F` creates limits of `K` if, given any limit cone `c` for `K ⋙ F`
+(i.e. below) we can lift it to a cone "above", and further that `F` reflects
+limits for `K`.
+-/
+
 open category_theory category_theory.limits
 
 noncomputable theory

src/category_theory/limits/types.lean

@@ -7,6 +7,18 @@ import category_theory.limits.shapes.images
 import category_theory.filtered
 import tactic.equiv_rw
 
+/-!
+# Limits in the category of types.
+
+We show that the category of types has all (co)limits, by providing the usual concrete models.
+
+We also give a characterisation of filtered colimits in `Type`, via
+`colimit.ι F i xi = colimit.ι F j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj`.
+
+Finally, we prove the category of types has categorical images,
+and that these agree with the range of a function.
+-/
+
 universes v u
 
 open category_theory

src/category_theory/monad/adjunction.lean

@@ -6,6 +6,23 @@ Authors: Scott Morrison, Bhavik Mehta
 import category_theory.adjunction.reflective
 import category_theory.monad.algebra
 
+/-!
+# Adjunctions and monads
+
+We develop the basic relationship between adjunctions and monads.
+
+Given an adjunction `h : L ⊣ R`, we have `h.to_monad : monad C` and `h.to_comonad : comonad D`.
+We then have
+`monad.comparison (h : L ⊣ R) : D ⥤ h.to_monad.algebra`
+sending `Y : D` to the Eilenberg-Moore algebra for `L ⋙ R` with underlying object `R.obj X`,
+and dually `comonad.comparison`.
+
+We say `R : D ⥤ C` is `monadic_right_adjoint`, if it is a right adjoint and its `monad.comparison`
+is an equivalence of categories. (Similarly for `monadic_left_adjoint`.)
+
+Finally we prove that reflective functors are `monadic_right_adjoint`.
+-/
+
 namespace category_theory
 open category
 

src/category_theory/monad/basic.lean

@@ -7,6 +7,18 @@ import category_theory.functor.category
 import category_theory.functor.fully_faithful
 import category_theory.functor.reflects_isomorphisms
 
+/-!
+# Monads
+
+We construct the categories of monads and comonads, and their forgetful functors to endofunctors.
+
+(Note that these are the category theorist's monads, not the programmers monads.
+For the translation, see the file `category_theory.monad.types`.)
+
+For the fact that monads are "just" monoids in the category of endofunctors, see the file
+`category_theory.monad.equiv_mon`.
+-/
+
 namespace category_theory
 open category