{P : Sort u_1} →
  {C : Type u} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {A : C} →
        {t : HomotopicalAlgebra.Precylinder A} →
          {C' : Type u} →
            {inst' : CategoryTheory.Category.{v, u} C'} →
              {A' : C'} →
                {t' : HomotopicalAlgebra.Precylinder A'} →
                  C = C' → inst ≍ inst' → A ≍ A' → t ≍ t' → HomotopicalAlgebra.Precylinder.noConfusionType P t t'