∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A I : C} {i₀ i₁ : A ⟶ I} {π : I ⟶ A}
  {i₀_π :
    autoParam (CategoryTheory.CategoryStruct.comp i₀ π = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₀_π._autoParam}
  {i₁_π :
    autoParam (CategoryTheory.CategoryStruct.comp i₁ π = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₁_π._autoParam}
  {I_1 : C} {i₀_1 i₁_1 : A ⟶ I_1} {π_1 : I_1 ⟶ A}
  {i₀_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i₀_1 π_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₀_π._autoParam}
  {i₁_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp i₁_1 π_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.Precylinder.i₁_π._autoParam},
  { I := I, i₀ := i₀, i₁ := i₁, π := π, i₀_π := i₀_π, i₁_π := i₁_π } =
      { I := I_1, i₀ := i₀_1, i₁ := i₁_1, π := π_1, i₀_π := i₀_π_1, i₁_π := i₁_π_1 } →
    I = I_1 ∧ i₀ ≍ i₀_1 ∧ i₁ ≍ i₁_1 ∧ π ≍ π_1