Theorems · Definition · category theory

CategoryTheory.Pretriangulated.noConfusion

{P : Sort u_1} →
  {C : Type u} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {inst_1 : CategoryTheory.Limits.HasZeroObject C} →
        {inst_2 : CategoryTheory.HasShift C ℤ} →
          {inst_3 : CategoryTheory.Preadditive C} →
            {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} →
              {t : CategoryTheory.Pretriangulated C} →
                {C' : Type u} →
                  {inst' : CategoryTheory.Category.{v, u} C'} →
                    {inst'_1 : CategoryTheory.Limits.HasZeroObject C'} →
                      {inst'_2 : CategoryTheory.HasShift C' ℤ} →
                        {inst'_3 : CategoryTheory.Preadditive C'} →
                          {inst'_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C' n).Additive} →
                            {t' : CategoryTheory.Pretriangulated C'} →
                              C = C' →
                                inst ≍ inst' →
                                  inst_1 ≍ inst'_1 →
                                    inst_2 ≍ inst'_2 →
                                      inst_3 ≍ inst'_3 →
                                        inst_4 ≍ inst'_4 →
                                          t ≍ t' → CategoryTheory.Pretriangulated.noConfusionType P t t'

Defined in

Mathlib.CategoryTheory.Triangulated.Pretriangulated

Cited by

0 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound