diff --git a/category_theory/category.lean b/category_theory/category.lean
index 1abea28e4bd0a..a7766a76f5f4b 100644
--- a/category_theory/category.lean
+++ b/category_theory/category.lean
@@ -58,6 +58,7 @@ restate_axiom category.id_comp'
 restate_axiom category.comp_id'
 restate_axiom category.assoc'
 attribute [simp] category.id_comp category.comp_id category.assoc
+attribute [trans] category.comp
 
 /--
 A `large_category` has objects in one universe level higher than the universe level of
diff --git a/category_theory/equivalence.lean b/category_theory/equivalence.lean
new file mode 100644
index 0000000000000..78d53f7fbe2f4
--- /dev/null
+++ b/category_theory/equivalence.lean
@@ -0,0 +1,274 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Tim Baumann, Stephen Morgan, Scott Morrison
+
+import category_theory.embedding
+import category_theory.functor_category
+import category_theory.natural_isomorphism
+import tactic.slice
+import tactic.converter.interactive
+
+namespace category_theory
+
+universes u₁ v₁ u₂ v₂ u₃ v₃
+
+structure equivalence (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] :=
+(functor : C ⥤ D)
+(inverse : D ⥤ C)
+(fun_inv_id' : (functor ⋙ inverse) ≅ (category_theory.functor.id C) . obviously)
+(inv_fun_id' : (inverse ⋙ functor) ≅ (category_theory.functor.id D) . obviously)
+
+restate_axiom equivalence.fun_inv_id'
+restate_axiom equivalence.inv_fun_id'
+
+infixr ` ≌ `:10  := equivalence
+
+namespace equivalence
+
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C]
+include 𝒞
+
+@[refl] def refl : C ≌ C :=
+{ functor := functor.id C,
+  inverse := functor.id C }
+
+variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒟
+
+@[symm] def symm (e : C ≌ D) : D ≌ C :=
+{ functor := e.inverse,
+  inverse := e.functor,
+  fun_inv_id' := e.inv_fun_id,
+  inv_fun_id' := e.fun_inv_id }
+
+@[simp] lemma fun_inv_map (e : C ≌ D) (X Y : D) (f : X ⟶ Y) :
+e.functor.map (e.inverse.map f) = (e.inv_fun_id.hom.app X) ≫ f ≫ (e.inv_fun_id.inv.app Y) :=
+begin
+  erw [nat_iso.naturality_2],
+  refl
+end
+@[simp] lemma inv_fun_map (e : C ≌ D) (X Y : C) (f : X ⟶ Y) :
+e.inverse.map (e.functor.map f) = (e.fun_inv_id.hom.app X) ≫ f ≫ (e.fun_inv_id.inv.app Y) :=
+begin
+  erw [nat_iso.naturality_2],
+  refl
+end
+
+variables {E : Type u₃} [ℰ : category.{u₃ v₃} E]
+include ℰ
+
+@[simp] private def effe_iso_id (e : C ≌ D) (f : D ≌ E) (X : C) :
+  (e.inverse).obj ((f.inverse).obj ((f.functor).obj ((e.functor).obj X))) ≅ X :=
+calc
+  (e.inverse).obj ((f.inverse).obj ((f.functor).obj ((e.functor).obj X)))
+    ≅ (e.inverse).obj ((e.functor).obj X) : e.inverse.on_iso (nat_iso.app f.fun_inv_id _)
+... ≅ X                                   : nat_iso.app e.fun_inv_id _
+
+@[simp] private def feef_iso_id (e : C ≌ D) (f : D ≌ E) (X : E) :
+  (f.functor).obj ((e.functor).obj ((e.inverse).obj ((f.inverse).obj X))) ≅ X :=
+calc
+  (f.functor).obj ((e.functor).obj ((e.inverse).obj ((f.inverse).obj X)))
+    ≅ (f.functor).obj ((f.inverse).obj X) : f.functor.on_iso (nat_iso.app e.inv_fun_id _)
+... ≅ X                                   : nat_iso.app f.inv_fun_id _
+
+@[trans] def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E :=
+{ functor := e.functor ⋙ f.functor,
+  inverse := f.inverse ⋙ e.inverse,
+  fun_inv_id' := nat_iso.of_components (effe_iso_id e f)
+  begin
+    /- `tidy` says -/
+    intros X Y f_1, dsimp at *, simp at *, dsimp at *,
+    /- `rewrite_search` says -/
+    conv_lhs { erw [←category.assoc] },
+    conv_lhs { congr, skip, erw [←category.assoc] },
+    conv_lhs { congr, skip, congr, erw [is_iso.hom_inv_id] },
+    conv_lhs { congr, skip, erw [category.id_comp] },
+    conv_lhs { erw [category.assoc] },
+    conv_lhs { congr, skip, erw [is_iso.hom_inv_id] },
+    conv_lhs { erw [category.comp_id] }
+  end,
+  inv_fun_id' := nat_iso.of_components (feef_iso_id e f)
+  begin
+    /- `tidy` says -/
+    intros X Y f_1, dsimp at *, simp at *, dsimp at *,
+    /- `rewrite_search` says -/
+    conv_lhs { erw [←category.assoc] },
+    conv_lhs { congr, skip, erw [←category.assoc] },
+    conv_lhs { congr, skip, congr, erw [is_iso.hom_inv_id] },
+    conv_lhs { congr, skip, erw [category.id_comp] },
+    conv_lhs { erw [category.assoc] },
+    conv_lhs { congr, skip, erw [is_iso.hom_inv_id] },
+    conv_lhs { erw [category.comp_id] }
+  end
+}
+
+end equivalence
+
+variables {C : Type u₁} [𝒞 : category.{u₁ v₁} C]
+include 𝒞
+
+section
+variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒟
+
+class is_equivalence (F : C ⥤ D) :=
+(inverse        : D ⥤ C)
+(fun_inv_id' : (F ⋙ inverse) ≅ (functor.id C) . obviously)
+(inv_fun_id' : (inverse ⋙ F) ≅ (functor.id D) . obviously)
+
+restate_axiom is_equivalence.fun_inv_id'
+restate_axiom is_equivalence.inv_fun_id'
+end
+
+namespace is_equivalence
+variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒟
+
+instance of_equivalence (F : C ≌ D) : is_equivalence (F.functor) :=
+{ inverse := F.inverse,
+  fun_inv_id' := F.fun_inv_id,
+  inv_fun_id' := F.inv_fun_id }
+instance of_equivalence_inverse (F : C ≌ D) : is_equivalence (F.inverse) :=
+{ inverse := F.functor,
+  fun_inv_id' := F.inv_fun_id,
+  inv_fun_id' := F.fun_inv_id }
+end is_equivalence
+
+namespace functor
+instance is_equivalence_refl : is_equivalence (functor.id C) :=
+{ inverse := functor.id C }
+end functor
+
+variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒟
+
+namespace functor
+def inv (F : C ⥤ D) [is_equivalence F] : D ⥤ C :=
+is_equivalence.inverse F
+
+instance is_equivalence_symm (F : C ⥤ D) [is_equivalence F] : is_equivalence (F.inv) :=
+{ inverse := F,
+  fun_inv_id' := is_equivalence.inv_fun_id F,
+  inv_fun_id' := is_equivalence.fun_inv_id F }
+
+def fun_inv_id (F : C ⥤ D) [is_equivalence F] : (F ⋙ F.inv) ≅ functor.id C :=
+is_equivalence.fun_inv_id F
+
+def inv_fun_id (F : C ⥤ D) [is_equivalence F] : (F.inv ⋙ F) ≅ functor.id D :=
+is_equivalence.inv_fun_id F
+
+def as_equivalence (F : C ⥤ D) [is_equivalence F] : C ≌ D :=
+{ functor := F,
+  inverse := is_equivalence.inverse F,
+  fun_inv_id' := is_equivalence.fun_inv_id F,
+  inv_fun_id' := is_equivalence.inv_fun_id F }
+
+variables {E : Type u₃} [ℰ : category.{u₃ v₃} E]
+include ℰ
+
+instance is_equivalence_trans (F : C ⥤ D) (G : D ⥤ E) [is_equivalence F] [is_equivalence G] :
+  is_equivalence (F ⋙ G) :=
+is_equivalence.of_equivalence (equivalence.trans (as_equivalence F) (as_equivalence G))
+
+end functor
+
+namespace is_equivalence
+instance is_equivalence_functor (e : C ≌ D) : is_equivalence e.functor :=
+{ inverse := e.inverse,
+  fun_inv_id' := e.fun_inv_id,
+  inv_fun_id' := e.inv_fun_id }
+instance is_equivalence_inverse (e : C ≌ D) : is_equivalence e.inverse :=
+{ inverse := e.functor,
+  fun_inv_id' := e.inv_fun_id,
+  inv_fun_id' := e.fun_inv_id }
+
+@[simp] lemma fun_inv_map (F : C ⥤ D) [is_equivalence F] (X Y : D) (f : X ⟶ Y) :
+  F.map (F.inv.map f) = (F.inv_fun_id.hom.app X) ≫ f ≫ (F.inv_fun_id.inv.app Y) :=
+begin
+  erw [nat_iso.naturality_2],
+  refl
+end
+@[simp] lemma inv_fun_map (F : C ⥤ D) [is_equivalence F] (X Y : C) (f : X ⟶ Y) :
+  F.inv.map (F.map f) = (F.fun_inv_id.hom.app X) ≫ f ≫ (F.fun_inv_id.inv.app Y) :=
+begin
+  erw [nat_iso.naturality_2],
+  refl
+end
+
+end is_equivalence
+
+class ess_surj (F : C ⥤ D) :=
+(obj_preimage (d : D) : C)
+(iso' (d : D) : F.obj (obj_preimage d) ≅ d . obviously)
+
+restate_axiom ess_surj.iso'
+
+namespace functor
+def obj_preimage (F : C ⥤ D) [ess_surj F] (d : D) : C := ess_surj.obj_preimage.{u₁ v₁ u₂ v₂} F d
+def fun_obj_preimage_iso (F : C ⥤ D) [ess_surj F] (d : D) : F.obj (F.obj_preimage d) ≅ d :=
+ess_surj.iso F d
+end functor
+
+namespace category_theory.equivalence
+
+def ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F :=
+⟨ λ Y : D, F.inv.obj Y, λ Y : D, (nat_iso.app F.inv_fun_id Y) ⟩
+
+instance faithful_of_equivalence (F : C ⥤ D) [is_equivalence F] : faithful F :=
+{ injectivity' := λ X Y f g w,
+  begin
+    have p := congr_arg (@category_theory.functor.map _ _ _ _ F.inv _ _) w,
+    simp at *,
+    assumption
+  end }.
+
+instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F :=
+{ preimage := λ X Y f, (nat_iso.app F.fun_inv_id X).inv ≫ (F.inv.map f) ≫ (nat_iso.app F.fun_inv_id Y).hom,
+  witness' := λ X Y f,
+  begin
+    apply F.inv.injectivity,
+    /- obviously can finish from here... -/
+    dsimp, simp, dsimp,
+    slice_lhs 4 6 {
+      rw [←functor.map_comp, ←functor.map_comp],
+      rw [←is_equivalence.fun_inv_map],
+    },
+    slice_lhs 1 2 { simp },
+    dsimp, simp,
+    slice_lhs 2 4 {
+      rw [←functor.map_comp, ←functor.map_comp],
+      erw [nat_iso.naturality_2],
+    },
+    erw [nat_iso.naturality_1],
+    refl,
+  end }.
+
+section
+
+@[simp] private def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : D ⥤ C :=
+{ obj  := λ X, F.obj_preimage X,
+  map := λ X Y f, F.preimage ((F.fun_obj_preimage_iso X).hom ≫ f ≫ (F.fun_obj_preimage_iso Y).inv),
+  map_id' := λ X, begin apply F.injectivity, tidy, end,
+  map_comp' := λ X Y Z f g,
+  begin
+    apply F.injectivity,
+    /- obviously can finish from here... -/
+    simp,
+    slice_rhs 2 3 { erw [is_iso.hom_inv_id] },
+    simp,
+  end }.
+
+def equivalence_of_fully_faithfully_ess_surj
+  (F : C ⥤ D) [full F] [faithful : faithful F] [ess_surj F] : is_equivalence F :=
+{ inverse := equivalence_inverse F,
+  fun_inv_id' := nat_iso.of_components
+    (λ X, preimage_iso (F.fun_obj_preimage_iso (F.obj X)))
+    (λ X Y f, begin apply F.injectivity, obviously, end),
+  inv_fun_id' := nat_iso.of_components
+    (λ Y, (F.fun_obj_preimage_iso Y))
+    (by obviously) }
+end
+
+end category_theory.equivalence
+
+end category_theory
\ No newline at end of file
diff --git a/category_theory/natural_isomorphism.lean b/category_theory/natural_isomorphism.lean
index 15cc7731ea109..629bc67767f28 100644
--- a/category_theory/natural_isomorphism.lean
+++ b/category_theory/natural_isomorphism.lean
@@ -37,6 +37,32 @@ instance inv_app_is_iso (α : F ≅ G) (X : C) : is_iso (α.inv.app X) :=
   hom_inv_id' := begin rw [←functor.category.comp_app, iso.inv_hom_id, ←functor.category.id_app] end,
   inv_hom_id' := begin rw [←functor.category.comp_app, iso.hom_inv_id, ←functor.category.id_app] end }
 
+@[simp] lemma hom_vcomp_inv (α : F ≅ G) : (α.hom ⊟ α.inv) = nat_trans.id _ :=
+begin
+  have h : (α.hom ⊟ α.inv) = α.hom ≫ α.inv := rfl,
+  rw h,
+  rw iso.hom_inv_id,
+  refl
+end
+@[simp] lemma inv_vcomp_hom (α : F ≅ G) : (α.inv ⊟ α.hom) = nat_trans.id _ :=
+begin
+  have h : (α.inv ⊟ α.hom) = α.inv ≫ α.hom := rfl,
+  rw h,
+  rw iso.inv_hom_id,
+  refl
+end
+
+@[simp] lemma hom_app_inv_app_id (α : F ≅ G) (X : C) : α.hom.app X ≫ α.inv.app X = 𝟙 _ :=
+begin
+  rw ←nat_trans.vcomp_app,
+  simp,
+end
+@[simp] lemma inv_app_hom_app_id (α : F ≅ G) (X : C) : α.inv.app X ≫ α.hom.app X = 𝟙 _ :=
+begin
+  rw ←nat_trans.vcomp_app,
+  simp,
+end
+
 variables {X Y : C}
 @[simp] lemma naturality_1 (α : F ≅ G) (f : X ⟶ Y) :
   (α.inv.app X) ≫ (F.map f) ≫ (α.hom.app Y) = G.map f :=
diff --git a/tactic/slice.lean b/tactic/slice.lean
new file mode 100644
index 0000000000000..6d90012be8819
--- /dev/null
+++ b/tactic/slice.lean
@@ -0,0 +1,91 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.category
+
+open category_theory
+
+-- TODO someone might like to generalise this tactic to work with other associative structures.
+
+namespace tactic
+
+meta def repeat_with_results {α : Type} (t : tactic α) : tactic (list α) :=
+(do r ← t,
+    s ← repeat_with_results,
+    return (r :: s)) <|> return []
+
+meta def repeat_count {α : Type} (t : tactic α) : tactic ℕ :=
+do r ← repeat_with_results t,
+   return r.length
+
+end tactic
+
+namespace conv
+open tactic
+meta def repeat_with_results {α : Type} (t : tactic α) : tactic (list α) :=
+(do r ← t,
+    s ← repeat_with_results,
+    return (r :: s)) <|> return []
+
+meta def repeat_count {α : Type} (t : tactic α) : tactic ℕ :=
+do r ← repeat_with_results t,
+   return r.length
+
+meta def slice (a b : ℕ) : conv unit :=
+do repeat $ to_expr ``(category.assoc) >>= λ e, tactic.rewrite_target e {symm:=ff},
+   iterate_range (a-1) (a-1) (do conv.congr, conv.skip),
+   k ← repeat_count $ to_expr ``(category.assoc) >>= λ e, tactic.rewrite_target e {symm:=tt},
+   iterate_range (k+1+a-b) (k+1+a-b) conv.congr,
+   repeat $ to_expr ``(category.assoc) >>= λ e, tactic.rewrite_target e {symm:=ff},
+   rotate 1,
+   iterate_exactly (k+1+a-b) conv.skip
+
+meta def slice_lhs (a b : ℕ) (t : conv unit) : tactic unit :=
+do conv.interactive.to_lhs,
+   slice a b,
+   t
+
+meta def slice_rhs (a b : ℕ) (t : conv unit) : tactic unit :=
+do conv.interactive.to_rhs,
+   slice a b,
+   t
+
+namespace interactive
+/--
+`slice` is a conv tactic; if the current focus is a composition of several morphisms,
+`slice a b` reassociates as needed, and zooms in on the `a`-th through `b`-th morphisms.
+
+Thus if the current focus is `(a ≫ b) ≫ ((c ≫ d) ≫ e)`, then `slice 2 3` zooms to `b ≫ c`.
+ -/
+meta def slice := conv.slice
+end interactive
+end conv
+
+namespace tactic
+open conv
+private meta def conv_target' (c : conv unit) : tactic unit :=
+do t ← target,
+   (new_t, pr) ← c.convert t,
+   replace_target new_t pr,
+   try tactic.triv, try (tactic.reflexivity reducible)
+
+namespace interactive
+open interactive
+open lean.parser
+
+/--
+`slice_lhs a b { tac }` zooms to the left hand side, uses associativity for categorical
+composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
+-/
+meta def slice_lhs (a b : parse small_nat) (t : conv.interactive.itactic) : tactic unit :=
+do conv_target' (conv.interactive.to_lhs >> slice a b >> t)
+/--
+`slice_rhs a b { tac }` zooms to the right hand side, uses associativity for categorical
+composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
+-/
+meta def slice_rhs (a b : parse small_nat) (t : conv.interactive.itactic) : tactic unit :=
+do conv_target' (conv.interactive.to_rhs >> slice a b >> t)
+end interactive
+end tactic
+