diff --git a/src/category_theory/const.lean b/src/category_theory/const.lean
index a88f7444b595e..13211cfe93cca 100644
--- a/src/category_theory/const.lean
+++ b/src/category_theory/const.lean
@@ -5,6 +5,17 @@ Authors: Scott Morrison, Bhavik Mehta
 -/
 import category_theory.opposites
 
+/-!
+# The constant functor
+
+`const J : C ⥤ (J ⥤ C)` is the functor that sends an object `X : C` to the functor `J ⥤ C` sending
+every object in `J` to `X`, and every morphism to `𝟙 X`.
+
+When `J` is nonempty, `const` is faithful.
+
+We have `(const J).obj X ⋙ F ≅ (const J).obj (F.obj X)` for any `F : C ⥤ D`.
+-/
+
 -- declare the `v`'s first; see `category_theory.category` for an explanation
 universes v₁ v₂ v₃ u₁ u₂ u₃
 
diff --git a/src/category_theory/core.lean b/src/category_theory/core.lean
index 92f5d71b6fe61..f7d61db123019 100644
--- a/src/category_theory/core.lean
+++ b/src/category_theory/core.lean
@@ -7,6 +7,18 @@ import category_theory.groupoid
 import control.equiv_functor
 import category_theory.types
 
+/-!
+# The core of a category
+
+The core of a category `C` is the (non-full) subcategory of `C` consisting of all objects,
+and all isomorphisms. We construct it as a `groupoid`.
+
+`core.inclusion : core C ⥤ C` gives the faithful inclusion into the original category.
+
+Any functor `F` from a groupoid `G` into `C` factors through `core C`,
+but this is not functorial with respect to `F`.
+-/
+
 namespace category_theory
 
 universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
@@ -29,12 +41,16 @@ namespace core
 @[simp] lemma comp_hom {X Y Z : core C} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).hom = f.hom ≫ g.hom :=
 rfl
 
+variables (C)
+
 /-- The core of a category is naturally included in the category. -/
 def inclusion : core C ⥤ C :=
 { obj := id,
   map := λ X Y f, f.hom }
 
-variables {G : Type u₂} [groupoid.{v₂} G]
+instance : faithful (inclusion C) := {}
+
+variables {C} {G : Type u₂} [groupoid.{v₂} G]
 
 /-- A functor from a groupoid to a category C factors through the core of C. -/
 -- Note that this function is not functorial
@@ -48,7 +64,7 @@ def functor_to_core (F : G ⥤ C) : G ⥤ core C :=
 We can functorially associate to any functor from a groupoid to the core of a category `C`,
 a functor from the groupoid to `C`, simply by composing with the embedding `core C ⥤ C`.
 -/
-def forget_functor_to_core : (G ⥤ core C) ⥤ (G ⥤ C) := (whiskering_right _ _ _).obj inclusion
+def forget_functor_to_core : (G ⥤ core C) ⥤ (G ⥤ C) := (whiskering_right _ _ _).obj (inclusion C)
 end core
 
 /--
diff --git a/src/category_theory/currying.lean b/src/category_theory/currying.lean
index d8d5393b89ee0..37780cb02fed1 100644
--- a/src/category_theory/currying.lean
+++ b/src/category_theory/currying.lean
@@ -5,6 +5,14 @@ Authors: Scott Morrison
 -/
 import category_theory.products.bifunctor
 
+/-!
+# Curry and uncurry, as functors.
+
+We define `curry : ((C × D) ⥤ E) ⥤ (C ⥤ (D ⥤ E))` and `uncurry : (C ⥤ (D ⥤ E)) ⥤ ((C × D) ⥤ E)`,
+and verify that they provide an equivalence of categories
+`currying : (C ⥤ (D ⥤ E)) ≌ ((C × D) ⥤ E)`.
+
+-/
 namespace category_theory
 
 universes v₁ v₂ v₃ u₁ u₂ u₃
diff --git a/src/category_theory/discrete_category.lean b/src/category_theory/discrete_category.lean
index b21b729c02c5d..b7d908b3e5441 100644
--- a/src/category_theory/discrete_category.lean
+++ b/src/category_theory/discrete_category.lean
@@ -5,6 +5,30 @@ Authors: Stephen Morgan, Scott Morrison, Floris van Doorn
 -/
 import category_theory.eq_to_hom
 
+/-!
+# Discrete categories
+
+We define `discrete α := α` for any type `α`, and use this type alias
+to provide a `small_category` instance whose only morphisms are the identities.
+
+There is an annoying technical difficulty that it has turned out to be inconvenient
+to allow categories with morphisms living in `Prop`,
+so instead of defining `X ⟶ Y` in `discrete α` as `X = Y`,
+one might define it as `plift (X = Y)`.
+In fact, to allow `discrete α` to be a `small_category`
+(i.e. with morphisms in the same universe as the objects),
+we actually define the hom type `X ⟶ Y` as `ulift (plift (X = Y))`.
+
+`discrete.functor` promotes a function `f : I → C` (for any category `C`) to a functor
+`discrete.functor f : discrete I ⥤ C`.
+
+Similarly, `discrete.nat_trans` and `discrete.nat_iso` promote `I`-indexed families of morphisms,
+or `I`-indexed families of isomorphisms to natural transformations or natural isomorphism.
+
+We show equivalences of types are the same as (categorical) equivalences of the corresponding
+discrete categories.
+-/
+
 namespace category_theory
 
 universes v₁ v₂ u₁ u₂ -- morphism levels before object levels. See note [category_theory universes].
diff --git a/src/category_theory/products/basic.lean b/src/category_theory/products/basic.lean
index a59eb3926712e..fc089dc6a3c38 100644
--- a/src/category_theory/products/basic.lean
+++ b/src/category_theory/products/basic.lean
@@ -5,6 +5,23 @@ Authors: Stephen Morgan, Scott Morrison
 -/
 import category_theory.eq_to_hom
 
+/-!
+# Cartesian products of categories
+
+We define the category instance on `C × D` when `C` and `D` are categories.
+
+We define:
+* `sectl C Z` : the functor `C ⥤ C × D` given by `X ↦ ⟨X, Z⟩`
+* `sectr Z D` : the functor `D ⥤ C × D` given by `Y ↦ ⟨Z, Y⟩`
+* `fst`       : the functor `⟨X, Y⟩ ↦ X`
+* `snd`       : the functor `⟨X, Y⟩ ↦ Y`
+* `swap`      : the functor `C × D ⥤ D × C` given by `⟨X, Y⟩ ↦ ⟨Y, X⟩`
+    (and the fact this is an equivalence)
+
+We further define `evaluation : C ⥤ (C ⥤ D) ⥤ D` and `evaluation_uncurried : C × (C ⥤ D) ⥤ D`,
+and products of functors and natural transformations, written `F.prod G` and `α.prod β`.
+-/
+
 namespace category_theory
 
 -- declare the `v`'s first; see `category_theory.category` for an explanation
diff --git a/src/category_theory/punit.lean b/src/category_theory/punit.lean
index 50d7fd3fa478d..32b9b68aa892b 100644
--- a/src/category_theory/punit.lean
+++ b/src/category_theory/punit.lean
@@ -6,6 +6,14 @@ Authors: Scott Morrison, Bhavik Mehta
 import category_theory.const
 import category_theory.discrete_category
 
+/-!
+# The category `discrete punit`
+
+We define `star : C ⥤ discrete punit` sending everything to `punit.star`,
+show that any two functors to `discrete punit` are naturally isomorphic,
+and construct the equivalence `(discrete punit ⥤ C) ≌ C`.
+-/
+
 universes v u -- morphism levels before object levels. See note [category_theory universes].
 
 namespace category_theory
diff --git a/src/category_theory/reflects_isomorphisms.lean b/src/category_theory/reflects_isomorphisms.lean
index a4ff876700ef9..de184c24aed0e 100644
--- a/src/category_theory/reflects_isomorphisms.lean
+++ b/src/category_theory/reflects_isomorphisms.lean
@@ -5,6 +5,16 @@ Authors: Bhavik Mehta
 -/
 import category_theory.fully_faithful
 
+/-!
+# Functors which reflect isomorphisms
+
+A functor `F` reflects isomorphisms if whenever `F.map f` is an isomorphism, `f` was too.
+
+It is formalized as a `Prop` valued typeclass `reflects_isomorphisms F`.
+
+Any fully faithful functor reflects isomorphisms.
+-/
+
 open category_theory
 
 namespace category_theory
@@ -21,7 +31,7 @@ Define what it means for a functor `F : C ⥤ D` to reflect isomorphisms: for an
 morphism `f : A ⟶ B`, if `F.map f` is an isomorphism then `f` is as well.
 Note that we do not assume or require that `F` is faithful.
 -/
-class reflects_isomorphisms (F : C ⥤ D) :=
+class reflects_isomorphisms (F : C ⥤ D) : Prop :=
 (reflects : Π {A B : C} (f : A ⟶ B) [is_iso (F.map f)], is_iso f)
 
 /-- If `F` reflects isos and `F.map f` is an iso, then `f` is an iso. -/
diff --git a/src/category_theory/simple.lean b/src/category_theory/simple.lean
index 999c89e3f611e..8b46b8889a879 100644
--- a/src/category_theory/simple.lean
+++ b/src/category_theory/simple.lean
@@ -7,6 +7,24 @@ import category_theory.limits.shapes.zero
 import category_theory.limits.shapes.kernels
 import category_theory.abelian.basic
 
+/-!
+# Simple objects
+
+We define simple objects in any category with zero morphisms.
+A simple object is an object `Y` such that any monomorphism `f : X ⟶ Y`
+is either an isomorphism or zero (but not both).
+
+This is formalized as a `Prop` valued typeclass `simple X`.
+
+If a morphism `f` out of a simple object is nonzero and has a kernel, then that kernel is zero.
+(We state this as `kernel.ι f = 0`, but should add `kernel f ≅ 0`.)
+
+When the category is abelian, being simple is the same as being cosimple (although we do not
+state a separate typeclass for this).
+As a consequence, any nonzero epimorphism out of a simple object is an isomorphism,
+and any nonzero morphism into a simple object has trivial cokernel.
+-/
+
 noncomputable theory
 
 open category_theory.limits
diff --git a/src/category_theory/sums/associator.lean b/src/category_theory/sums/associator.lean
index e6beda066040e..4905f7c7ebe7e 100644
--- a/src/category_theory/sums/associator.lean
+++ b/src/category_theory/sums/associator.lean
@@ -5,7 +5,9 @@ Authors: Scott Morrison
 -/
 import category_theory.sums.basic
 
-/-#
+/-!
+# Associator for binary disjoint union of categories.
+
 The associator functor `((C ⊕ D) ⊕ E) ⥤ (C ⊕ (D ⊕ E))` and its inverse form an equivalence.
 -/
 
diff --git a/src/category_theory/sums/basic.lean b/src/category_theory/sums/basic.lean
index c59f40d590bd3..56f891cf21bdc 100644
--- a/src/category_theory/sums/basic.lean
+++ b/src/category_theory/sums/basic.lean
@@ -5,8 +5,18 @@ Authors: Scott Morrison
 -/
 import category_theory.eq_to_hom
 
-/-#
-Disjoint unions of categories, functors, and natural transformations.
+/-!
+# Binary disjoint unions of categories
+
+We define the category instance on `C ⊕ D` when `C` and `D` are categories.
+
+We define:
+* `inl_`      : the functor `C ⥤ C ⊕ D`
+* `inr_`      : the functor `D ⥤ C ⊕ D`
+* `swap`      : the functor `C ⊕ D ⥤ D ⊕ C`
+    (and the fact this is an equivalence)
+
+We further define sums of functors and natural transformations, written `F.sum G` and `α.sum β`.
 -/
 
 namespace category_theory