{P : Sort u_1} →
  {C : Type u} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {inst_1 : CategoryTheory.HasShift C ℤ} →
        {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
          {t : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂} →
            {C' : Type u} →
              {inst' : CategoryTheory.Category.{v, u} C'} →
                {inst'_1 : CategoryTheory.HasShift C' ℤ} →
                  {T₁' T₂' : CategoryTheory.Pretriangulated.Triangle C'} →
                    {t' : CategoryTheory.Pretriangulated.TriangleMorphism T₁' T₂'} →
                      C = C' →
                        inst ≍ inst' →
                          inst_1 ≍ inst'_1 →
                            T₁ ≍ T₁' →
                              T₂ ≍ T₂' → t ≍ t' → CategoryTheory.Pretriangulated.TriangleMorphism.noConfusionType P t t'