∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {A : C} (P P' : HomotopicalAlgebra.PrepathObject A),
  CategoryTheory.CategoryStruct.comp P.ι P.p₁ = CategoryTheory.CategoryStruct.comp P'.ι P'.p₀