∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  {X Y : CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)}
  (q : Quot (CategoryTheory.HomRel.CompClosure (CategoryTheory.pathsHomRel C))),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id (CategoryTheory.Quotient (CategoryTheory.pathsHomRel C))).map q)
      (CategoryTheory.Quotient.casesOn (motive := fun t =>
          Y = t →
            ((CategoryTheory.Functor.id (CategoryTheory.Quotient (CategoryTheory.pathsHomRel C))).obj Y ≅
              ((CategoryTheory.quotientPathsTo C).comp (CategoryTheory.toQuotientPaths C)).obj Y))
          Y
          (fun as h =>
            ⋯ ▸
              CategoryTheory.Iso.refl
                ((CategoryTheory.Functor.id (CategoryTheory.Quotient (CategoryTheory.pathsHomRel C))).obj { as := as }))
          ⋯).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Quotient.casesOn (motive := fun t =>
          X = t →
            ((CategoryTheory.Functor.id (CategoryTheory.Quotient (CategoryTheory.pathsHomRel C))).obj X ≅
              ((CategoryTheory.quotientPathsTo C).comp (CategoryTheory.toQuotientPaths C)).obj X))
          X
          (fun as h =>
            ⋯ ▸
              CategoryTheory.Iso.refl
                ((CategoryTheory.Functor.id (CategoryTheory.Quotient (CategoryTheory.pathsHomRel C))).obj { as := as }))
          ⋯).hom
      (((CategoryTheory.quotientPathsTo C).comp (CategoryTheory.toQuotientPaths C)).map q)