diff --git a/src/algebra/category/Group/adjunctions.lean b/src/algebra/category/Group/adjunctions.lean
index f9ba10049cc4a..0c1aea407db72 100644
--- a/src/algebra/category/Group/adjunctions.lean
+++ b/src/algebra/category/Group/adjunctions.lean
@@ -29,8 +29,9 @@ free abelian group with generators `x : X`.
 def free : Type u ⥤ AddCommGroup.{u} :=
 { obj := λ α, of (free_abelian_group α),
   map := λ X Y f, add_monoid_hom.of (λ x : free_abelian_group X, f <$> x),
-  map_id' := λ X, add_monoid_hom.ext $ by simp,
-  map_comp' := λ X Y Z f g, add_monoid_hom.ext $ by { intro x, simp [is_lawful_functor.comp_map], } }
+  map_id' := λ X, add_monoid_hom.ext $ by simp [types_id],
+  map_comp' := λ X Y Z f g, add_monoid_hom.ext $
+    by { intro x, simp [is_lawful_functor.comp_map, types_comp], } }
 
 @[simp] lemma free_obj_coe {α : Type u} :
   (free.obj α : Type u) = (free_abelian_group α) := rfl
@@ -44,7 +45,8 @@ The free-forgetful adjunction for abelian groups.
 def adj : free ⊣ forget AddCommGroup.{u} :=
 adjunction.mk_of_hom_equiv
 { hom_equiv := λ X G, free_abelian_group.hom_equiv X G,
-  hom_equiv_naturality_left_symm' := by {intros, ext, dsimp at *, simp [free_abelian_group.lift_comp],} }
+  hom_equiv_naturality_left_symm' :=
+  by { intros, ext, simp [types_comp, free_abelian_group.lift_comp], } }
 
 /--
 As an example, we now give a high-powered proof that
diff --git a/src/category_theory/category/default.lean b/src/category_theory/category/default.lean
index dab2df494787e..85a4e8640f939 100644
--- a/src/category_theory/category/default.lean
+++ b/src/category_theory/category/default.lean
@@ -135,14 +135,14 @@ by { convert cancel_epi f, simp, }
 lemma cancel_mono_id (f : X ⟶ Y) [mono f] {g : X ⟶ X} : (g ≫ f = f) ↔ g = 𝟙 X :=
 by { convert cancel_mono f, simp, }
 
-instance epi_comp {X Y Z : C} (f : X ⟶ Y) [epi f] (g : Y ⟶ Z) [epi g] : epi (f ≫ g) :=
+lemma epi_comp {X Y Z : C} (f : X ⟶ Y) [epi f] (g : Y ⟶ Z) [epi g] : epi (f ≫ g) :=
 begin
   split, intros Z a b w,
   apply (cancel_epi g).1,
   apply (cancel_epi f).1,
   simpa using w,
 end
-instance mono_comp {X Y Z : C} (f : X ⟶ Y) [mono f] (g : Y ⟶ Z) [mono g] : mono (f ≫ g) :=
+lemma mono_comp {X Y Z : C} (f : X ⟶ Y) [mono f] (g : Y ⟶ Z) [mono g] : mono (f ≫ g) :=
 begin
   split, intros Z a b w,
   apply (cancel_mono f).1,
diff --git a/src/category_theory/limits/shapes/images.lean b/src/category_theory/limits/shapes/images.lean
index a98a568adeac7..11c7775137aaa 100644
--- a/src/category_theory/limits/shapes/images.lean
+++ b/src/category_theory/limits/shapes/images.lean
@@ -207,6 +207,7 @@ begin
   let F' : mono_factorisation f :=
   { I := equalizer g h,
     m := q ≫ image.ι f,
+    m_mono := by apply mono_comp,
     e := e' },
   let v := image.lift F',
   have t₀ : v ≫ q ≫ image.ι f = image.ι f := image.lift_fac F',
diff --git a/src/category_theory/types.lean b/src/category_theory/types.lean
index a6b92f782daf8..fc0e8d08d7cff 100644
--- a/src/category_theory/types.lean
+++ b/src/category_theory/types.lean
@@ -7,6 +7,29 @@ import category_theory.functor_category
 import category_theory.fully_faithful
 import data.equiv.basic
 
+/-!
+# The category `Type`.
+
+In this section we set up the theory so that Lean's types and functions between them
+can be viewed as a `large_category` in our framework.
+
+Lean can not transparently view a function as a morphism in this category,
+and needs a hint in order to be able to type check.
+We provide the abbreviation `as_hom f` to guide type checking,
+as well as a corresponding notation `↾ f`. (Entered as `\upr `.)
+
+We provide various simplification lemmas for functors and natural transformations valued in `Type`.
+
+We define `ulift_functor`, from `Type u` to `Type (max u v)`, and show that it is fully faithful
+(but not, of course, essentially surjective).
+
+We prove some basic facts about the category `Type`:
+*  epimorphisms are surjections and monomorphisms are injections,
+* `iso` is both `iso` and `equiv` to `equiv` (at least within a fixed universe),
+* every type level `is_lawful_functor` gives a categorical functor `Type ⥤ Type`
+  (the corresponding fact about monads is in `src/category_theory/monad/types.lean`).
+-/
+
 namespace category_theory
 
 universes v v' w u u' -- declare the `v`'s first; see `category_theory.category` for an explanation
@@ -16,14 +39,41 @@ instance types : large_category (Type u) :=
   id      := λ a, id,
   comp    := λ _ _ _ f g, g ∘ f }
 
-@[simp] lemma types_hom {α β : Type u} : (α ⟶ β) = (α → β) := rfl
-@[simp] lemma types_id (X : Type u) : 𝟙 X = id := rfl
-@[simp] lemma types_comp {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) : f ≫ g = g ∘ f := rfl
+lemma types_hom {α β : Type u} : (α ⟶ β) = (α → β) := rfl
+lemma types_id (X : Type u) : 𝟙 X = id := rfl
+lemma types_comp {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) : f ≫ g = g ∘ f := rfl
+
+@[simp]
+lemma types_id_apply (X : Type u) (x : X) : ((𝟙 X) : X → X) x = x := rfl
+@[simp]
+lemma types_comp_apply {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) : (f ≫ g) x = g (f x) := rfl
+
+
+/-- `as_hom f` helps Lean type check a function as a morphism in the category `Type`. -/
+-- Unfortunately without this wrapper we can't use `category_theory` idioms, such as `is_iso f`.
+abbreviation as_hom {α β : Type u} (f : α → β) : α ⟶ β := f
+-- If you don't mind some notation you can use fewer keystrokes:
+notation  `↾` f : 200 := as_hom f -- type as \upr in VScode
+
+section -- We verify the expected type checking behaviour of `as_hom`.
+variables (α β γ : Type u) (f : α → β) (g : β → γ)
+
+example : α → γ := ↾f ≫ ↾g
+example [is_iso ↾f] : mono ↾f := by apply_instance
+example [is_iso ↾f] : ↾f ≫ inv ↾f = 𝟙 α := by simp
+end
 
 namespace functor
 variables {J : Type u} [𝒥 : category.{v} J]
 include 𝒥
 
+/--
+The sections of a functor `J ⥤ Type` are
+the choices of a point `u j : F.obj j` for each `j`,
+such that `F.map f (u j) = u j` for every morphism `f : j ⟶ j'`.
+
+We later use these to define limits in `Type` and in many concrete categories.
+-/
 def sections (F : J ⥤ Type w) : set (Π j, F.obj j) :=
 { u | ∀ {j j'} (f : j ⟶ j'), F.map f (u j) = u j'}
 end functor
@@ -33,11 +83,11 @@ variables {C : Type u} [𝒞 : category.{v} C] (F G H : C ⥤ Type w) {X Y Z : C
 include 𝒞
 variables (σ : F ⟶ G) (τ : G ⟶ H)
 
-@[simp] lemma map_comp (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) : (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) :=
-by simp
+@[simp] lemma map_comp_apply (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) : (F.map (f ≫ g)) a = (F.map g) ((F.map f) a) :=
+by simp [types_comp]
 
-@[simp] lemma map_id (a : F.obj X) : (F.map (𝟙 X)) a = a :=
-by simp
+@[simp] lemma map_id_apply (a : F.obj X) : (F.map (𝟙 X)) a = a :=
+by simp [types_id]
 
 lemma naturality (f : X ⟶ Y) (x : F.obj X) : σ.app Y ((F.map f) x) = (G.map f) (σ.app X x) :=
 congr_fun (σ.naturality f) x
@@ -55,8 +105,16 @@ congr_fun (F.map_iso f).inv_hom_id y
 
 end functor_to_types
 
+/--
+The isomorphism between a `Type` which has been `ulift`ed to the same universe,
+and the original type.
+-/
 def ulift_trivial (V : Type u) : ulift.{u} V ≅ V := by tidy
 
+/--
+The functor embedding `Type u` into `Type (max u v)`.
+Write this as `ulift_functor.{5 2}` to get `Type 2 ⥤ Type 5`.
+-/
 def ulift_functor : Type u ⥤ Type (max u v) :=
 { obj := λ X, ulift.{v} X,
   map := λ X Y f, λ x : ulift.{v} X, ulift.up (f x.down) }
@@ -70,6 +128,9 @@ instance ulift_functor_faithful : faithful ulift_functor :=
 { injectivity' := λ X Y f g p, funext $ λ x,
     congr_arg ulift.down ((congr_fun p (ulift.up x)) : ((ulift.up (f x)) = (ulift.up (g x)))) }
 
+/-- Any term `x` of a type `X` corresponds to a morphism `punit ⟶ X`. -/
+-- TODO We should connect this to a general story about concrete categories
+-- whose forgetful functor is representable.
 def hom_of_element {X : Type u} (x : X) : punit ⟶ X := λ _, x
 
 lemma hom_of_element_eq_iff {X : Type u} (x y : X) :
@@ -148,6 +209,10 @@ universe u
 
 variables {X Y : Type u}
 
+/--
+Any equivalence between types in the same universe gives
+a categorical isomorphism between those types.
+-/
 def to_iso (e : X ≃ Y) : X ≅ Y :=
 { hom := e.to_fun,
   inv := e.inv_fun,
@@ -166,6 +231,9 @@ universe u
 
 variables {X Y : Type u}
 
+/--
+Any isomorphism between types gives an equivalence.
+-/
 def to_equiv (i : X ≅ Y) : X ≃ Y :=
 { to_fun := i.hom,
   inv_fun := i.inv,
diff --git a/src/category_theory/yoneda.lean b/src/category_theory/yoneda.lean
index aca86a3b0aff4..e1e87474c25d5 100644
--- a/src/category_theory/yoneda.lean
+++ b/src/category_theory/yoneda.lean
@@ -151,7 +151,7 @@ def yoneda_lemma : yoneda_pairing C ≅ yoneda_evaluation C :=
            ←functor_to_types.naturality,
            obj_map_id,
            functor_to_types.naturality,
-           functor_to_types.map_id]
+           functor_to_types.map_id_apply]
     end },
   inv :=
   { app := λ F x,
@@ -159,12 +159,12 @@ def yoneda_lemma : yoneda_pairing C ≅ yoneda_evaluation C :=
       naturality' :=
       begin
         intros X Y f, ext, dsimp,
-        rw [functor_to_types.map_comp]
+        rw [functor_to_types.map_comp_apply]
       end },
     naturality' :=
     begin
       intros X Y f, ext, dsimp,
-      rw [←functor_to_types.naturality, functor_to_types.map_comp]
+      rw [←functor_to_types.naturality, functor_to_types.map_comp_apply]
     end },
   hom_inv_id' :=
   begin
@@ -172,13 +172,13 @@ def yoneda_lemma : yoneda_pairing C ≅ yoneda_evaluation C :=
     erw [←functor_to_types.naturality,
          obj_map_id,
          functor_to_types.naturality,
-         functor_to_types.map_id],
+         functor_to_types.map_id_apply],
     refl,
   end,
   inv_hom_id' :=
   begin
     ext, dsimp,
-    rw [functor_to_types.map_id]
+    rw [functor_to_types.map_id_apply]
   end }.
 
 variables {C}
diff --git a/src/topology/metric_space/lipschitz.lean b/src/topology/metric_space/lipschitz.lean
index e861988d3e6db..703c63948b499 100644
--- a/src/topology/metric_space/lipschitz.lean
+++ b/src/topology/metric_space/lipschitz.lean
@@ -174,7 +174,7 @@ hf.comp hg
 endomorphism. -/
 protected lemma list_prod (f : ι → End α) (K : ι → ℝ≥0) (h : ∀ i, lipschitz_with (K i) (f i)) :
   ∀ l : list ι, lipschitz_with (l.map K).prod (l.map f).prod
-| [] := by simp [lipschitz_with.id]
+| [] := by simp [types_id, lipschitz_with.id]
 | (i :: l) := by { simp only [list.map_cons, list.prod_cons], exact (h i).mul (list_prod l) }
 
 protected lemma pow {f : End α} {K} (h : lipschitz_with K f) :