∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
  Quot.mk (CategoryTheory.HomRel.CompClosure (CategoryTheory.pathsHomRel C))
      (CategoryTheory.CategoryStruct.comp f g).toPath =
    Quot.mk (CategoryTheory.HomRel.CompClosure (CategoryTheory.pathsHomRel C))
      (CategoryTheory.CategoryStruct.comp f.toPath g.toPath)