diff --git a/src/category_theory/adjunction.lean b/src/category_theory/adjunction.lean
new file mode 100644
index 0000000000000..0b161837e11c7
--- /dev/null
+++ b/src/category_theory/adjunction.lean
@@ -0,0 +1,393 @@
+/-
+Copyright (c) 2019 Reid Barton. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Reid Barton, Johan Commelin
+-/
+
+import category_theory.limits.preserves
+import category_theory.whiskering
+import category_theory.equivalence
+
+namespace category_theory
+open category
+open category_theory.limits
+
+universes v₁ v₂ v₃ u₁ u₂ u₃ -- declare the `v`'s first; see `category_theory.category` for an explanation
+
+local attribute [elab_simple] whisker_left whisker_right
+
+variables {C : Type u₁} [𝒞 : category.{v₁} C] {D : Type u₂} [𝒟 : category.{v₂} D]
+include 𝒞 𝒟
+
+/--
+`adjunction F G` represents the data of an adjunction between two functors
+`F : C ⥤ D` and `G : D ⥤ C`. `F` is the left adjoint and `G` is the right adjoint.
+-/
+structure adjunction (F : C ⥤ D) (G : D ⥤ C) :=
+(hom_equiv : Π (X Y), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
+(unit : functor.id C ⟶ F.comp G)
+(counit : G.comp F ⟶ functor.id D)
+(hom_equiv_unit' : Π {X Y f}, (hom_equiv X Y) f = (unit : _ ⟹ _).app X ≫ G.map f . obviously)
+(hom_equiv_counit' : Π {X Y g}, (hom_equiv X Y).symm g = F.map g ≫ counit.app Y . obviously)
+
+namespace adjunction
+
+restate_axiom hom_equiv_unit'
+restate_axiom hom_equiv_counit'
+attribute [simp, priority 1] hom_equiv_unit hom_equiv_counit
+
+section
+
+variables {F : C ⥤ D} {G : D ⥤ C} (adj : adjunction F G) {X' X : C} {Y Y' : D}
+
+@[simp, priority 1] lemma hom_equiv_naturality_left_symm (f : X' ⟶ X) (g : X ⟶ G.obj Y) :
+  (adj.hom_equiv X' Y).symm (f ≫ g) = F.map f ≫ (adj.hom_equiv X Y).symm g :=
+by rw [hom_equiv_counit, F.map_comp, assoc, adj.hom_equiv_counit.symm]
+
+@[simp] lemma hom_equiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
+  (adj.hom_equiv X' Y) (F.map f ≫ g) = f ≫ (adj.hom_equiv X Y) g :=
+by rw [← equiv.eq_symm_apply]; simp [-hom_equiv_unit]
+
+@[simp, priority 1] lemma hom_equiv_naturality_right (f : F.obj X ⟶ Y) (g : Y ⟶ Y') :
+  (adj.hom_equiv X Y') (f ≫ g) = (adj.hom_equiv X Y) f ≫ G.map g :=
+by rw [hom_equiv_unit, G.map_comp, ← assoc, ←hom_equiv_unit]
+
+@[simp] lemma hom_equiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
+  (adj.hom_equiv X Y').symm (f ≫ G.map g) = (adj.hom_equiv X Y).symm f ≫ g :=
+by rw [equiv.symm_apply_eq]; simp [-hom_equiv_counit]
+
+@[simp] lemma left_triangle :
+  (whisker_right adj.unit F).vcomp (whisker_left F adj.counit) = nat_trans.id _ :=
+begin
+  ext1 X, dsimp,
+  erw [← adj.hom_equiv_counit, equiv.symm_apply_eq, adj.hom_equiv_unit],
+  simp
+end
+
+@[simp] lemma right_triangle :
+  (whisker_left G adj.unit).vcomp (whisker_right adj.counit G) = nat_trans.id _ :=
+begin
+  ext1 Y, dsimp,
+  erw [← adj.hom_equiv_unit, ← equiv.eq_symm_apply, adj.hom_equiv_counit],
+  simp
+end
+
+@[simp] lemma left_triangle_components :
+  F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 _ :=
+congr_arg (λ (t : _ ⟹ functor.id C ⋙ F), t.app X) adj.left_triangle
+
+@[simp] lemma right_triangle_components {Y : D} :
+  adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 _ :=
+congr_arg (λ (t : _ ⟹ G ⋙ functor.id C), t.app Y) adj.right_triangle
+
+end
+
+structure core_hom_equiv (F : C ⥤ D) (G : D ⥤ C) :=
+(hom_equiv : Π (X Y), (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
+(hom_equiv_naturality_left_symm' : Π {X' X Y} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
+  (hom_equiv X' Y).symm (f ≫ g) = F.map f ≫ (hom_equiv X Y).symm g . obviously)
+(hom_equiv_naturality_right' : Π {X Y Y'} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
+  (hom_equiv X Y') (f ≫ g) = (hom_equiv X Y) f ≫ G.map g . obviously)
+
+namespace core_hom_equiv
+
+restate_axiom hom_equiv_naturality_left_symm'
+restate_axiom hom_equiv_naturality_right'
+attribute [simp, priority 1] hom_equiv_naturality_left_symm hom_equiv_naturality_right
+
+variables {F : C ⥤ D} {G : D ⥤ C} (adj : core_hom_equiv F G) {X' X : C} {Y Y' : D}
+
+@[simp] lemma hom_equiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
+  (adj.hom_equiv X' Y) (F.map f ≫ g) = f ≫ (adj.hom_equiv X Y) g :=
+by rw [← equiv.eq_symm_apply]; simp
+
+@[simp] lemma hom_equiv_naturality_right_symm (f : X ⟶ G.obj Y) (g : Y ⟶ Y') :
+  (adj.hom_equiv X Y').symm (f ≫ G.map g) = (adj.hom_equiv X Y).symm f ≫ g :=
+by rw [equiv.symm_apply_eq]; simp
+
+end core_hom_equiv
+
+structure core_unit_counit (F : C ⥤ D) (G : D ⥤ C) :=
+(unit : functor.id C ⟶ F.comp G)
+(counit : G.comp F ⟶ functor.id D)
+(left_triangle' : (whisker_right unit F).vcomp (whisker_left F counit) = nat_trans.id _ . obviously)
+(right_triangle' : (whisker_left G unit).vcomp (whisker_right counit G) = nat_trans.id _ . obviously)
+
+namespace core_unit_counit
+
+restate_axiom left_triangle'
+restate_axiom right_triangle'
+attribute [simp] left_triangle right_triangle
+
+end core_unit_counit
+
+variables (F : C ⥤ D) (G : D ⥤ C)
+
+def mk_of_hom_equiv (adj : core_hom_equiv F G) : adjunction F G :=
+{ unit :=
+  { app := λ X, (adj.hom_equiv X (F.obj X)) (𝟙 (F.obj X)),
+    naturality' :=
+    begin
+      intros,
+      erw [← adj.hom_equiv_naturality_left, ← adj.hom_equiv_naturality_right],
+      dsimp, simp
+    end },
+  counit :=
+  { app := λ Y, (adj.hom_equiv _ _).inv_fun (𝟙 (G.obj Y)),
+    naturality' :=
+    begin
+      intros,
+      erw [← adj.hom_equiv_naturality_left_symm, ← adj.hom_equiv_naturality_right_symm],
+      dsimp, simp
+    end },
+  hom_equiv_unit' := λ X Y f, by erw [← adj.hom_equiv_naturality_right]; simp,
+  hom_equiv_counit' := λ X Y f, by erw [← adj.hom_equiv_naturality_left_symm]; simp,
+  .. adj }
+
+def mk_of_unit_counit (adj : core_unit_counit F G) : adjunction F G :=
+{ hom_equiv := λ X Y,
+  { to_fun := λ f, adj.unit.app X ≫ G.map f,
+    inv_fun := λ g, F.map g ≫ adj.counit.app Y,
+    left_inv := λ f, begin
+      change F.map (_ ≫ _) ≫ _ = _,
+      rw [F.map_comp, assoc, ←functor.comp_map, adj.counit.naturality, ←assoc],
+      convert id_comp _ f,
+      exact congr_arg (λ t : _ ⟹ _, t.app _) adj.left_triangle
+    end,
+    right_inv := λ g, begin
+      change _ ≫ G.map (_ ≫ _) = _,
+      rw [G.map_comp, ←assoc, ←functor.comp_map, ←adj.unit.naturality, assoc],
+      convert comp_id _ g,
+      exact congr_arg (λ t : _ ⟹ _, t.app _) adj.right_triangle
+  end },
+  .. adj }
+
+section
+omit 𝒟
+
+def id : adjunction (functor.id C) (functor.id C) :=
+{ hom_equiv := λ X Y, equiv.refl _,
+  unit := 𝟙 _,
+  counit := 𝟙 _ }
+
+end
+
+/-
+TODO
+* define adjoint equivalences
+* show that every equivalence can be improved into an adjoint equivalence
+-/
+
+section
+variables {E : Type u₃} [ℰ : category.{v₃} E] (H : D ⥤ E) (I : E ⥤ D)
+
+def comp (adj₁ : adjunction F G) (adj₂ : adjunction H I) : adjunction (F ⋙ H) (I ⋙ G) :=
+{ hom_equiv := λ X Z, equiv.trans (adj₂.hom_equiv _ _) (adj₁.hom_equiv _ _),
+  unit := adj₁.unit ≫
+  (whisker_left F $ whisker_right adj₂.unit G) ≫ (functor.associator _ _ _).inv,
+  counit := (functor.associator _ _ _).hom ≫
+    (whisker_left I $ whisker_right adj₁.counit H) ≫ adj₂.counit }
+
+end
+
+structure is_left_adjoint (left : C ⥤ D) :=
+(right : D ⥤ C)
+(adj : adjunction left right)
+
+structure is_right_adjoint (right : D ⥤ C) :=
+(left : C ⥤ D)
+(adj : adjunction left right)
+
+section construct_left
+-- Construction of a left adjoint. In order to construct a left
+-- adjoint to a functor G : D → C, it suffices to give the object part
+-- of a functor F : C → D together with isomorphisms Hom(FX, Y) ≃
+-- Hom(X, GY) natural in Y. The action of F on morphisms can be
+-- constructed from this data.
+variables {F_obj : C → D} {G}
+variables (e : Π X Y, (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
+variables (he : Π X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g)
+include he
+
+private lemma he' {X Y Y'} (f g) : (e X Y').symm (f ≫ G.map g) = (e X Y).symm f ≫ g :=
+by intros; rw [equiv.symm_apply_eq, he]; simp
+
+def left_adjoint_of_equiv : C ⥤ D :=
+{ obj := F_obj,
+  map := λ X X' f, (e X (F_obj X')).symm (f ≫ e X' (F_obj X') (𝟙 _)),
+  map_comp' := λ X X' X'' f f', begin
+    rw [equiv.symm_apply_eq, he, equiv.apply_inverse_apply],
+    conv { to_rhs, rw [assoc, ←he, id_comp, equiv.apply_inverse_apply] },
+    simp
+  end }
+
+def adjunction_of_equiv_left : adjunction (left_adjoint_of_equiv e he) G :=
+mk_of_hom_equiv (left_adjoint_of_equiv e he) G
+{ hom_equiv := e,
+  hom_equiv_naturality_left_symm' :=
+  begin
+    intros,
+    erw [← he' e he, ← equiv.apply_eq_iff_eq],
+    simp [(he _ _ _ _ _).symm]
+  end }
+
+end construct_left
+
+section construct_right
+-- Construction of a right adjoint, analogous to the above.
+variables {F} {G_obj : D → C}
+variables (e : Π X Y, (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
+variables (he : Π X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g)
+include he
+
+private lemma he' {X' X Y} (f g) : F.map f ≫ (e X Y).symm g = (e X' Y).symm (f ≫ g) :=
+by intros; rw [equiv.eq_symm_apply, he]; simp
+
+def right_adjoint_of_equiv : D ⥤ C :=
+{ obj := G_obj,
+  map := λ Y Y' g, (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 _) ≫ g),
+  map_comp' := λ Y Y' Y'' g g', begin
+    rw [← equiv.eq_symm_apply, ← he' e he, equiv.inverse_apply_apply],
+    conv { to_rhs, rw [← assoc, he' e he, comp_id, equiv.inverse_apply_apply] },
+    simp
+  end }
+
+def adjunction_of_equiv_right : adjunction F (right_adjoint_of_equiv e he) :=
+mk_of_hom_equiv F (right_adjoint_of_equiv e he)
+{ hom_equiv := e,
+  hom_equiv_naturality_left_symm' := by intros; rw [equiv.symm_apply_eq, he]; simp,
+  hom_equiv_naturality_right' :=
+  begin
+    intros X Y Y' g h,
+    erw [←he, equiv.apply_eq_iff_eq, ←assoc, he' e he, comp_id, equiv.inverse_apply_apply]
+  end }
+
+end construct_right
+
+end adjunction
+
+end category_theory
+
+namespace category_theory.adjunction
+open category_theory
+open category_theory.functor
+open category_theory.limits
+
+universes u₁ u₂ v
+
+variables {C : Type u₁} [𝒞 : category.{v} C] {D : Type u₂} [𝒟 : category.{v} D]
+include 𝒞 𝒟
+
+variables {F : C ⥤ D} {G : D ⥤ C} (adj : adjunction F G)
+include adj
+
+section preservation_colimits
+variables {J : Type v} [small_category J] (K : J ⥤ C)
+
+def functoriality_is_left_adjoint :
+  is_left_adjoint (@cocones.functoriality _ _ _ _ K _ _ F) :=
+{ right := (cocones.functoriality G) ⋙ (cocones.precompose
+    (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv)),
+  adj := mk_of_unit_counit _ _
+  { unit :=
+    { app := λ c,
+      { hom := adj.unit.app c.X,
+        w' := λ j, by have := adj.unit.naturality (c.ι.app j); tidy },
+      naturality' := λ _ _ f, by have := adj.unit.naturality (f.hom); tidy },
+    counit :=
+    { app := λ c,
+      { hom := adj.counit.app c.X,
+        w' :=
+        begin
+          intro j,
+          dsimp,
+          erw [category.comp_id, category.id_comp, F.map_comp, category.assoc,
+            adj.counit.naturality (c.ι.app j), ← category.assoc,
+            adj.left_triangle_components, category.id_comp],
+          refl,
+        end },
+      naturality' := λ _ _ f, by have := adj.counit.naturality (f.hom); tidy } } }
+
+/-- A left adjoint preserves colimits. -/
+def left_adjoint_preserves_colimits : preserves_colimits F :=
+λ J 𝒥 K, by resetI; exact
+{ preserves := λ c hc, is_colimit_iso_unique_cocone_morphism.inv
+    (λ s, (((adj.functoriality_is_left_adjoint _).adj).hom_equiv _ _).unique_of_equiv $
+      is_colimit_iso_unique_cocone_morphism.hom hc _ ) }
+
+end preservation_colimits
+
+section preservation_limits
+variables {J : Type v} [small_category J] (K : J ⥤ D)
+
+def functoriality_is_right_adjoint :
+  is_right_adjoint (@cones.functoriality _ _ _ _ K _ _ G) :=
+{ left := (cones.functoriality F) ⋙ (cones.postcompose
+    ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom)),
+  adj := mk_of_unit_counit _ _
+  { unit :=
+    { app := λ c,
+      { hom := adj.unit.app c.X,
+        w' :=
+        begin
+          intro j,
+          dsimp,
+          erw [category.comp_id, category.id_comp, G.map_comp, ← category.assoc,
+            ← adj.unit.naturality (c.π.app j), category.assoc,
+            adj.right_triangle_components, category.comp_id],
+          refl,
+        end },
+      naturality' := λ _ _ f, by have := adj.unit.naturality (f.hom); tidy },
+    counit :=
+    { app := λ c,
+      { hom := adj.counit.app c.X,
+        w' := λ j, by have := adj.counit.naturality (c.π.app j); tidy },
+      naturality' := λ _ _ f, by have := adj.counit.naturality (f.hom); tidy } } }
+
+/-- A right adjoint preserves limits. -/
+def right_adjoint_preserves_limits : preserves_limits G :=
+λ J 𝒥 K, by resetI; exact
+{ preserves := λ c hc, is_limit_iso_unique_cone_morphism.inv
+    (λ s, (((adj.functoriality_is_right_adjoint _).adj).hom_equiv _ _).symm.unique_of_equiv $
+      is_limit_iso_unique_cone_morphism.hom hc _) }
+
+end preservation_limits
+
+-- Note: this is natural in K, but we do not yet have the tools to formulate that.
+def cocones_iso {J : Type v} [small_category J] {K : J ⥤ C} :
+  (cocones J D).obj (K ⋙ F) ≅ G ⋙ ((cocones J C).obj K) :=
+nat_iso.of_components (λ Y,
+{ hom := λ t,
+    { app := λ j, (adj.hom_equiv (K.obj j) Y) (t.app j),
+      naturality' := λ j j' f, by erw [← adj.hom_equiv_naturality_left, t.naturality]; dsimp; simp },
+  inv := λ t,
+    { app := λ j, (adj.hom_equiv (K.obj j) Y).symm (t.app j),
+      naturality' := λ j j' f, begin
+        erw [← adj.hom_equiv_naturality_left_symm, ← adj.hom_equiv_naturality_right_symm, t.naturality],
+        dsimp, simp
+      end } } )
+begin
+  intros Y₁ Y₂ f,
+  ext1 t,
+  ext1 j,
+  apply adj.hom_equiv_naturality_right
+end
+
+-- Note: this is natural in K, but we do not yet have the tools to formulate that.
+def cones_iso {J : Type v} [small_category J] {K : J ⥤ D} :
+  F.op ⋙ ((cones J D).obj K) ≅ (cones J C).obj (K ⋙ G) :=
+nat_iso.of_components (λ X,
+{ hom := λ t,
+  { app := λ j, (adj.hom_equiv X (K.obj j)) (t.app j),
+    naturality' := λ j j' f, begin
+      erw [← adj.hom_equiv_naturality_right, ← t.naturality, category.id_comp, category.id_comp],
+      refl
+    end },
+  inv := λ t,
+  { app := λ j, (adj.hom_equiv X (K.obj j)).symm (t.app j),
+    naturality' := λ j j' f, begin
+      erw [← adj.hom_equiv_naturality_right_symm, ← t.naturality, category.id_comp, category.id_comp]
+    end } } )
+(by tidy)
+
+end category_theory.adjunction
diff --git a/src/category_theory/category.lean b/src/category_theory/category.lean
index 0315d722286f0..81ac1f14f833b 100644
--- a/src/category_theory/category.lean
+++ b/src/category_theory/category.lean
@@ -100,29 +100,28 @@ structure concrete_category {c : Type u → Type v}
   hom ia ib f → hom ib ic g → hom ia ic (g ∘ f))
 attribute [class] concrete_category
 
-instance {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
-  [h : concrete_category @hom] : category (bundled c) :=
+section
+variables {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
+variables [h : concrete_category @hom]
+include h
+
+instance : category (bundled c) :=
 { hom   := λa b, subtype (hom a.2 b.2),
   id    := λa, ⟨@id a.1, h.hom_id a.2⟩,
   comp  := λa b c f g, ⟨g.1 ∘ f.1, h.hom_comp a.2 b.2 c.2 f.2 g.2⟩ }
 
-@[simp] lemma concrete_category_id
-  {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
-  [h : concrete_category @hom] (X : bundled c) : subtype.val (𝟙 X) = id := rfl
-@[simp] lemma concrete_category_comp
-  {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
-  [h : concrete_category @hom] {X Y Z : bundled c} (f : X ⟶ Y) (g : Y ⟶ Z) :
+@[simp] lemma concrete_category_id (X : bundled c) : subtype.val (𝟙 X) = id := rfl
+@[simp] lemma concrete_category_comp {X Y Z : bundled c} (f : X ⟶ Y) (g : Y ⟶ Z) :
   subtype.val (f ≫ g) = g.val ∘ f.val := rfl
 
-instance {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
-  [h : concrete_category @hom] {R S : bundled c} : has_coe_to_fun (R ⟶ S) :=
-{ F := λ f, R → S,
+instance {X Y : bundled c} : has_coe_to_fun (X ⟶ Y) :=
+{ F := λ f, X → Y,
   coe := λ f, f.1 }
 
-@[simp] lemma bundled_hom_coe
-  {c : Type u → Type v} (hom : ∀{α β : Type u}, c α → c β → (α → β) → Prop)
-  [h : concrete_category @hom] {R S : bundled c} (val : R → S) (prop) (r : R) :
-  (⟨val, prop⟩ : R ⟶ S) r = val r := rfl
+@[simp] lemma bundled_hom_coe {X Y : bundled c} (val : X → Y) (prop) (x : X) :
+  (⟨val, prop⟩ : X ⟶ Y) x = val x := rfl
+
+end
 
 section
 variables {C : Type u} [𝒞 : category.{v} C] {X Y Z : C}
diff --git a/src/category_theory/examples/monoids.lean b/src/category_theory/examples/monoids.lean
index 84f53780e9188..b3ea42465e3d9 100644
--- a/src/category_theory/examples/monoids.lean
+++ b/src/category_theory/examples/monoids.lean
@@ -8,7 +8,9 @@ Currently only the basic setup.
 -/
 
 import category_theory.fully_faithful
-import algebra.ring
+import category_theory.types
+import category_theory.adjunction
+import data.finsupp
 
 universes u v
 
diff --git a/src/category_theory/examples/rings.lean b/src/category_theory/examples/rings.lean
index d604b650e114b..6e517b7c4b92d 100644
--- a/src/category_theory/examples/rings.lean
+++ b/src/category_theory/examples/rings.lean
@@ -9,6 +9,8 @@ Currently only the basic setup.
 
 import category_theory.examples.monoids
 import category_theory.fully_faithful
+import category_theory.adjunction
+import linear_algebra.multivariate_polynomial
 import algebra.ring
 
 universes u v
@@ -40,23 +42,99 @@ instance : category CommRing :=
   id := λ R, ⟨ id, by resetI; apply_instance ⟩,
   comp := λ R S T g h, ⟨ h.1 ∘ g.1, begin haveI := g.2, haveI := h.2, apply_instance end ⟩ }
 
-instance CommRing_hom_coe {R S : CommRing} : has_coe_to_fun (R ⟶ S) :=
+namespace CommRing
+variables {R S T : CommRing.{u}}
+
+@[simp] lemma id_val : subtype.val (𝟙 R) = id := rfl
+@[simp] lemma comp_val (f : R ⟶ S) (g : S ⟶ T) :
+  (f ≫ g).val = g.val ∘ f.val := rfl
+
+instance hom_coe : has_coe_to_fun (R ⟶ S) :=
 { F := λ f, R → S,
   coe := λ f, f.1 }
 
-@[simp] lemma CommRing_hom_coe_app {R S : CommRing} (f : R ⟶ S) (r : R) : f r = f.val r := rfl
+@[simp] lemma hom_coe_app (f : R ⟶ S) (r : R) : f r = f.val r := rfl
 
-instance CommRing_hom_is_ring_hom {R S : CommRing} (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
+instance hom_is_ring_hom (f : R ⟶ S) : is_ring_hom (f : R → S) := f.2
+
+def Int : CommRing := ⟨ℤ, infer_instance⟩
+
+def Int.cast {R : CommRing} : Int ⟶ R := { val := int.cast, property := by apply_instance }
+
+def int.eq_cast' {R : Type u} [ring R] (f : int → R) [is_ring_hom f] : f = int.cast :=
+funext $ int.eq_cast f (is_ring_hom.map_one f) (λ _ _, is_ring_hom.map_add f)
+
+def Int.hom_unique {R : CommRing} : unique (Int ⟶ R) :=
+{ default := Int.cast,
+  uniq := λ f, subtype.ext.mpr $ funext $ int.eq_cast f f.2.map_one f.2.map_add }
+
+/-- The forgetful functor commutative rings to Type. -/
+def forget : CommRing.{u} ⥤ Type u :=
+{ obj := λ R, R,
+  map := λ _ _ f, f }
+
+instance forget.faithful : faithful (forget) := {}
+
+/-- The functor from commutative rings to rings. -/
+def to_Ring : CommRing.{u} ⥤ Ring.{u} :=
+{ obj := λ X, { α := X.1, str := by apply_instance },
+  map := λ X Y f, ⟨ f, by apply_instance ⟩ }
+
+instance to_Ring.faithful : faithful (to_Ring) := {}
 
-namespace CommRing
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
-def forget_to_CommMon : CommRing ⥤ CommMon :=
+def forget_to_CommMon : CommRing.{u} ⥤ CommMon.{u} :=
 { obj := λ X, { α := X.1, str := by apply_instance },
   map := λ X Y f, ⟨ f, by apply_instance ⟩ }
 
-instance : faithful (forget_to_CommMon) := {}
+instance forget_to_CommMon.faithful : faithful (forget_to_CommMon) := {}
 
 example : faithful (forget_to_CommMon ⋙ CommMon.forget_to_Mon) := by apply_instance
+
+section
+open mv_polynomial
+local attribute [instance, priority 0] subtype.fintype set_fintype classical.prop_decidable
+
+noncomputable def polynomial : Type u ⥤ CommRing.{u} :=
+{ obj := λ α, ⟨mv_polynomial α ℤ, by apply_instance⟩,
+  map := λ α β f, ⟨eval₂ C (X ∘ f), by apply_instance⟩,
+  map_id' := λ α, subtype.ext.mpr $ funext $ eval₂_eta,
+  map_comp' := λ α β γ f g, subtype.ext.mpr $ funext $ λ p,
+  by apply mv_polynomial.induction_on p; intros;
+    simp only [*, eval₂_add, eval₂_mul, eval₂_C, eval₂_X, comp_val,
+      eq_self_iff_true, function.comp_app, types_comp] at * }
+
+@[simp] lemma polynomial_obj_α {α : Type u} :
+  (polynomial.obj α).α = mv_polynomial α ℤ := rfl
+
+@[simp] lemma polynomial_map_val {α β : Type u} {f : α → β} :
+  (polynomial.map f).val = eval₂ C (X ∘ f) := rfl
+
+noncomputable def adj : adjunction polynomial (forget : CommRing ⥤ Type u) :=
+adjunction.mk_of_hom_equiv _ _
+{ hom_equiv := λ α R,
+  { to_fun := λ f, f ∘ X,
+    inv_fun := λ f, ⟨eval₂ int.cast f, by apply_instance⟩,
+    left_inv := λ f, subtype.ext.mpr $ funext $ λ p,
+    begin
+      have H0 := λ n, (congr (int.eq_cast' (f.val ∘ C)) (rfl : n = n)).symm,
+      have H1 := λ p₁ p₂, (@is_ring_hom.map_add _ _ _ _ f.val f.2 p₁ p₂).symm,
+      have H2 := λ p₁ p₂, (@is_ring_hom.map_mul _ _ _ _ f.val f.2 p₁ p₂).symm,
+      apply mv_polynomial.induction_on p; intros;
+      simp only [*, eval₂_add, eval₂_mul, eval₂_C, eval₂_X,
+        eq_self_iff_true, function.comp_app, hom_coe_app] at *
+    end,
+    right_inv := by tidy },
+  hom_equiv_naturality_left_symm' := λ X' X Y f g, subtype.ext.mpr $ funext $ λ p,
+  begin
+    apply mv_polynomial.induction_on p; intros;
+    simp only [*, eval₂_mul, eval₂_add, eval₂_C, eval₂_X,
+      comp_val, equiv.coe_fn_symm_mk, hom_coe_app, polynomial_map_val,
+      eq_self_iff_true, function.comp_app, add_right_inj, types_comp] at *
+  end }
+
+end
+
 end CommRing
 
 end category_theory.examples
diff --git a/src/category_theory/examples/topological_spaces.lean b/src/category_theory/examples/topological_spaces.lean
index 96d2bf75cbaa7..1af80d876c656 100644
--- a/src/category_theory/examples/topological_spaces.lean
+++ b/src/category_theory/examples/topological_spaces.lean
@@ -4,7 +4,7 @@
 
 import category_theory.full_subcategory
 import category_theory.functor_category
-import category_theory.limits.preserves
+import category_theory.adjunction
 import category_theory.limits.types
 import category_theory.natural_isomorphism
 import category_theory.eq_to_hom
@@ -73,6 +73,33 @@ instance : preserves_colimits (forget : Top.{u} ⥤ Type u) :=
   (colimit.is_colimit F) (colimit.is_colimit (F ⋙ forget))
 
 end
+
+def discrete : Type u ⥤ Top.{u} :=
+{ obj := λ X, ⟨X, ⊤⟩,
+  map := λ X Y f, ⟨f, continuous_top⟩ }
+
+def trivial : Type u ⥤ Top.{u} :=
+{ obj := λ X, ⟨X, ⊥⟩,
+  map := λ X Y f, ⟨f, continuous_bot⟩ }
+
+def adj₁ : adjunction discrete forget :=
+{ hom_equiv := λ X Y,
+  { to_fun := λ f, f,
+    inv_fun := λ f, ⟨f, continuous_top⟩,
+    left_inv := by tidy,
+    right_inv := by tidy },
+  unit := { app := λ X, id },
+  counit := { app := λ X, ⟨id, continuous_top⟩ } }
+
+def adj₂ : adjunction forget trivial :=
+{ hom_equiv := λ X Y,
+  { to_fun := λ f, ⟨f, continuous_bot⟩,
+    inv_fun := λ f, f,
+    left_inv := by tidy,
+    right_inv := by tidy },
+  unit := { app := λ X, ⟨id, continuous_bot⟩ },
+  counit := { app := λ X, id } }
+
 end Top
 
 variables {X : Top.{u}}
diff --git a/src/category_theory/fully_faithful.lean b/src/category_theory/fully_faithful.lean
index 866165b105496..07aaf23bc1b37 100644
--- a/src/category_theory/fully_faithful.lean
+++ b/src/category_theory/fully_faithful.lean
@@ -13,7 +13,7 @@ include 𝒞 𝒟
 
 class full (F : C ⥤ D) :=
 (preimage : ∀ {X Y : C} (f : (F.obj X) ⟶ (F.obj Y)), X ⟶ Y)
-(witness'  : ∀ {X Y : C} (f : (F.obj X) ⟶ (F.obj Y)), F.map (preimage f) = f . obviously)
+(witness' : ∀ {X Y : C} (f : (F.obj X) ⟶ (F.obj Y)), F.map (preimage f) = f . obviously)
 
 restate_axiom full.witness'
 attribute [simp] full.witness
@@ -28,7 +28,7 @@ def injectivity (F : C ⥤ D) [faithful F] {X Y : C} {f g : X ⟶ Y} (p : F.map
 faithful.injectivity F p
 
 def preimage (F : C ⥤ D) [full F] {X Y : C} (f : F.obj X ⟶ F.obj Y) : X ⟶ Y :=
-full.preimage.{v₁ v₂}  f
+full.preimage.{v₁ v₂} f
 @[simp] lemma image_preimage (F : C ⥤ D) [full F] {X Y : C} (f : F.obj X ⟶ F.obj Y) :
   F.map (preimage F f) = f :=
 by unfold preimage; obviously
diff --git a/src/category_theory/limits/cones.lean b/src/category_theory/limits/cones.lean
index a2ffe14ab3d57..88a38f97565b9 100644
--- a/src/category_theory/limits/cones.lean
+++ b/src/category_theory/limits/cones.lean
@@ -34,6 +34,9 @@ def cones : Cᵒᵖ ⥤ Type v := (const Jᵒᵖ ⋙ op_inv J C) ⋙ (yoneda.obj
 
 lemma cones_obj (X : C) : F.cones.obj X = ((const J).obj X ⟹ F) := rfl
 
+@[simp] lemma cones_map_app {X₁ X₂ : C} (f : X₁ ⟶ X₂) (t : F.cones.obj X₂) (j : J) :
+(F.cones.map f t).app j = f ≫ t.app j := rfl
+
 /--
 `F.cocones` is the functor assigning to an object `X` the type of
 natural transformations from `F` to the constant functor with value `X`.
@@ -43,6 +46,9 @@ def cocones : C ⥤ Type v := (const J) ⋙ (coyoneda.obj F)
 
 lemma cocones_obj (X : C) : F.cocones.obj X = (F ⟹ (const J).obj X) := rfl
 
+@[simp] lemma cocones_map_app {X₁ X₂ : C} (f : X₁ ⟶ X₂) (t : F.cocones.obj X₁) (j : J) :
+(F.cocones.map f t).app j = t.app j ≫ f := rfl
+
 end functor
 
 section
@@ -113,10 +119,6 @@ namespace cone
 { X := X,
   π := c.extensions.app X f }
 
-def postcompose {G : J ⥤ C} (α : F ⟹ G) (c : cone F) : cone G :=
-{ X := c.X,
-  π := c.π ⊟ α }
-
 def whisker {K : Type v} [small_category K] (E : K ⥤ J) (c : cone F) : cone (E ⋙ F) :=
 { X := c.X,
   π := whisker_left E c.π }
@@ -135,10 +137,6 @@ namespace cocone
 { X := X,
   ι := c.extensions.app X f }
 
-def precompose {G : J ⥤ C} (α : G ⟹ F) (c : cocone F) : cocone G :=
-{ X := c.X,
-  ι := α ⊟ c.ι }
-
 def whisker {K : Type v} [small_category K] (E : K ⥤ J) (c : cocone F) : cocone (E ⋙ F) :=
 { X := c.X,
   ι := whisker_left E c.ι }
@@ -178,6 +176,20 @@ namespace cones
 { hom := { hom := φ.hom },
   inv := { hom := φ.inv, w' := λ j, φ.inv_comp_eq.mpr (w j) } }
 
+def postcompose {G : J ⥤ C} (α : F ⟶ G) : cone F ⥤ cone G :=
+{ obj := λ c, { X := c.X, π := c.π ⊟ α },
+  map := λ c₁ c₂ f, { hom := f.hom, w' :=
+  by intro; erw ← category.assoc; simp [-category.assoc] } }
+
+@[simp] lemma postcompose_obj_X {G : J ⥤ C} (α : F ⟶ G) (c : cone F) :
+  ((postcompose α).obj c).X = c.X := rfl
+
+@[simp] lemma postcompose_obj_π {G : J ⥤ C} (α : F ⟶ G) (c : cone F) :
+  ((postcompose α).obj c).π = c.π ⊟ α := rfl
+
+@[simp] lemma postcompose_map_hom {G : J ⥤ C} (α : F ⟶ G) {c₁ c₂ : cone F} (f : c₁ ⟶ c₂):
+  ((postcompose α).map f).hom = f.hom := rfl
+
 section
 variables {D : Type u'} [𝒟 : category.{v} D]
 include 𝒟
@@ -224,6 +236,19 @@ namespace cocones
 { hom := { hom := φ.hom },
   inv := { hom := φ.inv, w' := λ j, φ.comp_inv_eq.mpr (w j).symm } }
 
+def precompose {G : J ⥤ C} (α : G ⟶ F) : cocone F ⥤ cocone G :=
+{ obj := λ c, { X := c.X, ι := α ⊟ c.ι },
+  map := λ c₁ c₂ f, { hom := f.hom } }
+
+@[simp] lemma precompose_obj_X {G : J ⥤ C} (α : G ⟶ F) (c : cocone F) :
+  ((precompose α).obj c).X = c.X := rfl
+
+@[simp] lemma precompose_obj_ι {G : J ⥤ C} (α : G ⟶ F) (c : cocone F) :
+  ((precompose α).obj c).ι = α ⊟ c.ι := rfl
+
+@[simp] lemma precompose_map_hom {G : J ⥤ C} (α : G ⟶ F) {c₁ c₂ : cocone F} (f : c₁ ⟶ c₂) :
+  ((precompose α).map f).hom = f.hom := rfl
+
 section
 variables {D : Type u'} [𝒟 : category.{v} D]
 include 𝒟
@@ -265,3 +290,4 @@ def map_cocone_morphism {c c' : cocone F} (f : cocone_morphism c c') :
 end functor
 
 end category_theory
+
diff --git a/src/category_theory/limits/limits.lean b/src/category_theory/limits/limits.lean
index bb9bdee843872..e826e1da1a1c3 100644
--- a/src/category_theory/limits/limits.lean
+++ b/src/category_theory/limits/limits.lean
@@ -119,6 +119,15 @@ def of_faithful {t : cone F} {D : Type u'} [category.{v} D] (G : C ⥤ D) [faith
 
 end is_limit
 
+def is_limit_iso_unique_cone_morphism {t : cone F} :
+  is_limit t ≅ Π s, unique (s ⟶ t) :=
+{ hom := λ h s,
+  { default := h.lift_cone_morphism s,
+    uniq := λ _, h.uniq_cone_morphism },
+  inv := λ h,
+  { lift := λ s, (h s).default.hom,
+    uniq' := λ s f w, congr_arg cone_morphism.hom ((h s).uniq ⟨f, w⟩) } }
+
 /-- A cocone `t` on `F` is a colimit cocone if each cocone on `F` admits a unique
   cocone morphism from `t`. -/
 structure is_colimit (t : cocone F) :=
@@ -221,6 +230,15 @@ def of_faithful {t : cocone F} {D : Type u'} [category.{v} D] (G : C ⥤ D) [fai
 
 end is_colimit
 
+def is_colimit_iso_unique_cocone_morphism {t : cocone F} :
+  is_colimit t ≅ Π s, unique (t ⟶ s) :=
+{ hom := λ h s,
+  { default := h.desc_cocone_morphism s,
+    uniq := λ _, h.uniq_cocone_morphism },
+  inv := λ h,
+  { desc := λ s, (h s).default.hom,
+    uniq' := λ s f w, congr_arg cocone_morphism.hom ((h s).uniq ⟨f, w⟩) } }
+
 section limit
 
 /-- `has_limit F` represents a particular chosen limit of the diagram `F`. -/
@@ -389,7 +407,7 @@ variables {F} {G : J ⥤ C} (α : F ⟹ G)
 by apply is_limit.fac
 
 @[simp] lemma limit.lift_map (c : cone F) :
-  limit.lift F c ≫ lim.map α = limit.lift G (c.postcompose α) :=
+  limit.lift F c ≫ lim.map α = limit.lift G ((cones.postcompose α).obj c) :=
 by ext; rw [assoc, lim.map_π, ←assoc, limit.lift_π, limit.lift_π]; refl
 
 lemma limit.map_pre {K : Type v} [small_category K] [has_limits_of_shape K C] (E : K ⥤ J) :
@@ -607,7 +625,7 @@ variables {F} {G : J ⥤ C} (α : F ⟹ G)
 by apply is_colimit.fac
 
 @[simp] lemma colimit.map_desc (c : cocone G) :
-  colim.map α ≫ colimit.desc G c = colimit.desc F (c.precompose α) :=
+  colim.map α ≫ colimit.desc G c = colimit.desc F ((cocones.precompose α).obj c) :=
 by ext; rw [←assoc, colim.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]; refl
 
 lemma colimit.pre_map {K : Type v} [small_category K] [has_colimits_of_shape K C] (E : K ⥤ J) :
@@ -634,9 +652,8 @@ begin
 end
 
 def colim_coyoneda : colim.op ⋙ coyoneda ≅ category_theory.cocones J C :=
-nat_iso.of_components (λ F, nat_iso.of_components (colimit.hom_iso F)
-  (by {tidy, dsimp [functor.cocones], rw category.assoc }))
-  (by {tidy, rw [← category.assoc,← category.assoc], tidy })
+nat_iso.of_components (λ F, nat_iso.of_components (colimit.hom_iso F) (by tidy))
+  (by {tidy, rw [← category.assoc,← category.assoc], tidy})
 
 end colim_functor
 
diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index 2902fd4fed75c..c8eed852bd744 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -471,12 +471,12 @@ def decidable_eq_of_equiv [decidable_eq β] (e : α ≃ β) : decidable_eq α
 def inhabited_of_equiv [inhabited β] (e : α ≃ β) : inhabited α :=
 ⟨e.symm (default _)⟩
 
-def unique_of_equiv [unique β] (e : α ≃ β) : unique α :=
+def unique_of_equiv (e : α ≃ β) (h : unique β) : unique α :=
 unique.of_surjective e.symm.bijective.2
 
 def unique_congr (e : α ≃ β) : unique α ≃ unique β :=
-{ to_fun := λ h, by resetI; exact e.symm.unique_of_equiv,
-  inv_fun := λ h, by resetI; exact e.unique_of_equiv,
+{ to_fun := e.symm.unique_of_equiv,
+  inv_fun := e.unique_of_equiv,
   left_inv := λ _, subsingleton.elim _ _,
   right_inv := λ _, subsingleton.elim _ _ }