chore(category_theory/*): doc-strings (#4453)

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

src/category_theory/endomorphism.lean

@@ -23,6 +23,7 @@ section struct
 variables {C : Type u} [category_struct.{v} C] (X : C)
 
 instance has_one : has_one (End X) := ⟨𝟙 X⟩
+instance inhabited : inhabited (End X) := ⟨𝟙 X⟩
 
 /-- Multiplication of endomorphisms agrees with `function.comp`, not `category_struct.comp`. -/
 instance has_mul : has_mul (End X) := ⟨λ x y, y ≫ x⟩
@@ -50,12 +51,20 @@ end End
 
 variables {C : Type u} [category.{v} C] (X : C)
 
+/--
+Automorphisms of an object in a category.
+
+The order of arguments in multiplication agrees with
+`function.comp`, not with `category.comp`.
+-/
 def Aut (X : C) := X ≅ X
 
 attribute [ext Aut] iso.ext
 
 namespace Aut
 
+instance inhabited : inhabited (Aut X) := ⟨iso.refl X⟩
+
 instance : group (Aut X) :=
 by refine { one := iso.refl X,
             inv := iso.symm,

src/category_theory/groupoid.lean

@@ -20,7 +20,15 @@ restate_axiom groupoid.comp_inv'
 
 attribute [simp] groupoid.inv_comp groupoid.comp_inv
 
+/--
+A `large_groupoid` is a groupoid
+where the objects live in `Type (u+1)` while the morphisms live in `Type u`.
+-/
 abbreviation large_groupoid (C : Type (u+1)) : Type (u+1) := groupoid.{u} C
+/--
+A `small_groupoid` is a groupoid
+where the objects and morphisms live in the same universe.
+-/
 abbreviation small_groupoid (C : Type u) : Type (u+1) := groupoid.{u} C
 
 section

src/category_theory/monoidal/functor.lean

@@ -75,9 +75,15 @@ attribute [instance] monoidal_functor.ε_is_iso monoidal_functor.μ_is_iso
 
 variables {C D}
 
+/--
+The unit morphism of a (strong) monoidal functor as an isomorphism.
+-/
 def monoidal_functor.ε_iso (F : monoidal_functor.{v₁ v₂} C D) :
   tensor_unit D ≅ F.obj (tensor_unit C) :=
 as_iso F.ε
+/--
+The tensorator of a (strong) monoidal functor as an isomorphism.
+-/
 def monoidal_functor.μ_iso (F : monoidal_functor.{v₁ v₂} C D) (X Y : C) :
   (F.obj X) ⊗ (F.obj Y) ≅ F.obj (X ⊗ Y) :=
 as_iso (F.μ X Y)
@@ -96,6 +102,8 @@ variables (C : Type u₁) [category.{v₁} C] [monoidal_category.{v₁} C]
   μ := λ X Y, 𝟙 _,
   .. 𝟭 C }
 
+instance : inhabited (lax_monoidal_functor C C) := ⟨id C⟩
+
 end lax_monoidal_functor
 
 namespace monoidal_functor
@@ -141,6 +149,8 @@ variables (C : Type u₁) [category.{v₁} C] [monoidal_category.{v₁} C]
   μ := λ X Y, 𝟙 _,
   .. 𝟭 C }
 
+instance : inhabited (monoidal_functor C C) := ⟨id C⟩
+
 end
 
 end monoidal_functor