diff --git a/src/category_theory/path_category.lean b/src/category_theory/path_category.lean
index 6623c1350a54d..963973e54270a 100644
--- a/src/category_theory/path_category.lean
+++ b/src/category_theory/path_category.lean
@@ -4,10 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.eq_to_hom
+import category_theory.quotient
 import combinatorics.quiver.path
 
 /-!
 # The category paths on a quiver.
+When `C` is a quiver, `paths C` is the category of paths.
+
+## When the quiver is itself a category
+We provide `path_composition : paths C ⥤ C`.
+
+We check that the quotient of the path category of a category by the canonical relation
+(paths are related if they compose to the same path) is equivalent to the original category.
 -/
 
 universes v₁ v₂ u₁ u₂
@@ -85,6 +93,10 @@ def compose_path {X : C} : Π {Y : C} (p : path X Y), X ⟶ Y
 | _ path.nil := 𝟙 X
 | _ (path.cons p e) := compose_path p ≫ e
 
+@[simp]
+lemma compose_path_to_path {X Y : C} (f : X ⟶ Y) : compose_path (f.to_path) = f :=
+category.id_comp _
+
 @[simp]
 lemma compose_path_comp {X Y Z : C} (f : path X Y) (g : path Y Z) :
   compose_path (f.comp g) = compose_path f ≫ compose_path g :=
@@ -94,6 +106,64 @@ begin
   { simp [ih], },
 end
 
+@[simp]
+lemma compose_path_id {X : paths C} : compose_path (𝟙 X) = 𝟙 X := rfl
+
+@[simp]
+lemma compose_path_comp' {X Y Z : paths C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+  compose_path (f ≫ g) = compose_path f ≫ compose_path g :=
+compose_path_comp f g
+
+variables (C)
+
+/-- Composition of paths as functor from the path category of a category to the category. -/
+@[simps]
+def path_composition : paths C ⥤ C :=
+{ obj := λ X, X,
+  map := λ X Y f, compose_path f, }
+
+/-- The canonical relation on the path category of a category:
+two paths are related if they compose to the same morphism. -/
+-- TODO: This, and what follows, should be generalized to
+-- the `hom_rel` for the kernel of any functor.
+-- Indeed, this should be part of an equivalence between congruence relations on a category `C`
+-- and full, essentially surjective functors out of `C`.
+@[simp]
+def paths_hom_rel : hom_rel (paths C) :=
+λ X Y p q, (path_composition C).map p = (path_composition C).map q
+
+/-- The functor from a category to the canonical quotient of its path category. -/
+@[simps]
+def to_quotient_paths : C ⥤ quotient (paths_hom_rel C) :=
+{ obj := λ X, quotient.mk X,
+  map := λ X Y f, quot.mk _ f.to_path,
+  map_id' := λ X, quot.sound (quotient.comp_closure.of _ _ _ (by simp)),
+  map_comp' := λ X Y Z f g, quot.sound (quotient.comp_closure.of _ _ _ (by simp)), }
+
+/-- The functor from the canonical quotient of a path category of a category
+to the original category. -/
+@[simps]
+def quotient_paths_to : quotient (paths_hom_rel C) ⥤ C :=
+quotient.lift _ (path_composition C) (λ X Y p q w, w)
+
+/-- The canonical quotient of the path category of a category
+is equivalent to the original category. -/
+def quotient_paths_equiv : quotient (paths_hom_rel C) ≌ C :=
+{ functor := quotient_paths_to C,
+  inverse := to_quotient_paths C,
+  unit_iso := nat_iso.of_components (λ X, by { cases X, refl, }) begin
+    intros,
+    cases X, cases Y,
+    induction f,
+    dsimp,
+    simp only [category.comp_id, category.id_comp],
+    apply quot.sound,
+    apply quotient.comp_closure.of,
+    simp [paths_hom_rel],
+  end,
+  counit_iso := nat_iso.of_components (λ X, iso.refl _) (by tidy),
+  functor_unit_iso_comp' := by { intros, cases X, dsimp, simp, refl, }, }
+
 end
 
 end category_theory
diff --git a/src/category_theory/quotient.lean b/src/category_theory/quotient.lean
index 4bea125ea7b4d..94b63d2b1c21d 100644
--- a/src/category_theory/quotient.lean
+++ b/src/category_theory/quotient.lean
@@ -50,6 +50,9 @@ inductive comp_closure ⦃s t : C⦄ : (s ⟶ t) → (s ⟶ t) → Prop
 | intro {a b} (f : s ⟶ a) (m₁ m₂ : a ⟶ b) (g : b ⟶ t) (h : r m₁ m₂) :
   comp_closure (f ≫ m₁ ≫ g) (f ≫ m₂ ≫ g)
 
+lemma comp_closure.of {a b} (m₁ m₂ : a ⟶ b) (h : r m₁ m₂) : comp_closure r m₁ m₂ :=
+by simpa using comp_closure.intro (𝟙 _) m₁ m₂ (𝟙 _) h
+
 lemma comp_left {a b c : C} (f : a ⟶ b) : Π (g₁ g₂ : b ⟶ c) (h : comp_closure r g₁ g₂),
   comp_closure r (f ≫ g₁) (f ≫ g₂)
 | _ _ ⟨x, m₁, m₂, y, h⟩ := by simpa using comp_closure.intro (f ≫ x) m₁ m₂ y h