{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {A : C} →
      {P : Sort u_1} →
        {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' : 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 := I, i₀ := i₀, i₁ := i₁, π := π, i₀_π := i₀_π, i₁_π := i₁_π } =
                                { I := I', i₀ := i₀', i₁ := i₁', π := π', i₀_π := i₀_π', i₁_π := i₁_π' } →
                              (I ≍ I' → i₀ ≍ i₀' → i₁ ≍ i₁' → π ≍ π' → P) → P