wording: add a bunch of descriptions

Author: plt-amy

src/Cat/Functor/Adjoint.lagda.md

@@ -1,3 +1,10 @@
+---
+description: |
+  We present two definitions of adjoint functors, one which is
+  computationally convenient (units and counits), and one which is
+  conceptually clean (adjoints as "optimal solutions" --- initial
+  objects in certain comma categories).
+---
 ```agda
 open import Cat.Diagram.Initial
 open import Cat.Instances.Comma

src/Cat/Functor/Adjoint/Compose.lagda.md

@@ -1,3 +1,6 @@
+---
+description: We compute the composite of two adjunctions.
+---
 ```agda
 open import Cat.Functor.Adjoint
 open import Cat.Prelude

src/Cat/Functor/Adjoint/Continuous.lagda.md

@@ -1,3 +1,6 @@
+---
+description: We establish that right adjoints preserve limits.
+---
 ```agda
 open import Cat.Diagram.Colimit.Base
 open import Cat.Diagram.Limit.Finite

src/Cat/Functor/Adjoint/Hom.lagda.md

@@ -1,3 +1,9 @@
+---
+description: |
+  We establish a correspondence between adjoint functors in terms of
+  units and counits and in terms of satisfying a certain natural
+  isomorphism of Hom-sets.
+---
 ```agda
 open import Cat.Functor.Adjoint
 open import Cat.Prelude

src/Cat/Functor/Adjoint/Monad.lagda.md

@@ -1,3 +1,6 @@
+---
+description: We define the monad associated to an adjunction.
+---
 ```agda
 open import Cat.Functor.Adjoint
 open import Cat.Diagram.Monad

src/Cat/Functor/Adjoint/Monadic.lagda.md

@@ -1,3 +1,9 @@
+---
+description: |
+  We establish the theory of monadic adjunctions, and define the
+  comparison functor into the Eilenberg-Moore category for the induced
+  monad.
+---
 ```agda
 open import Cat.Functor.Adjoint.Monad
 open import Cat.Functor.Equivalence

src/Cat/Functor/Adjoint/Reflective.lagda.md

@@ -1,3 +1,11 @@
+---
+description: |
+  We characterise the *reflective subcategory* inclusions: the fully
+  faithful functors which have a left adjoint, equivalently which induce
+  an idempotent monad. We show that every reflective subcategory
+  inclusion is a monadic functor.
+---
+
 ```agda
 open import Cat.Functor.Adjoint.Monadic
 open import Cat.Functor.Equivalence

src/Cat/Functor/Amnestic.lagda.md

@@ -1,3 +1,8 @@
+---
+description: |
+  We establish the theory of amnestic functors, those which reflect
+  univalence of categories.
+---
 ```agda
 open import Cat.Functor.Base
 open import Cat.Prelude

src/Cat/Functor/Kan/Nerve.lagda.md

@@ -1,3 +1,10 @@
+---
+description: |
+  We use the calculation of left Kan extensions as certain colimits to
+  associate a "nerve" (restricted Yoneda embedding) and "realization"
+  (left Kan extension along よ) adjunction given any functor.
+---
+
 ```agda
 open import Cat.Instances.Shape.Terminal
 open import Cat.Diagram.Colimit.Base

src/Cat/Functor/Monadic/Beck.lagda.md

@@ -1,3 +1,8 @@
+---
+description: |
+  We define Beck's coequalisers, and establish their role in the crude
+  monadicity theorem.
+---
 ```agda
 open import Cat.Functor.Adjoint.Monadic
 open import Cat.Functor.Adjoint.Monad