∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} (P : HomotopicalAlgebra.Precylinder X) {Y : C}
  (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp P.i₀ (CategoryTheory.CategoryStruct.comp P.π f) = f