{C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {inst_1 : CategoryTheory.Preadditive C} →
      {inst_2 : CategoryTheory.Limits.HasZeroObject C} →
        {inst_3 : CategoryTheory.HasShift C ℤ} →
          {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} →
            {inst_5 : CategoryTheory.Pretriangulated C} →
              {t : CategoryTheory.Triangulated.TStructure C} →
                {H : Type u'} →
                  {inst_6 : CategoryTheory.Category.{v', u'} H} →
                    {inst_7 : CategoryTheory.Preadditive H} →
                      {P : Sort u_1} →
                        {ι : CategoryTheory.Functor H C} →
                          {additive_ι :
                              autoParam ι.Additive CategoryTheory.Triangulated.TStructure.Heart.additive_ι._autoParam} →
                            {full_ι : autoParam ι.Full CategoryTheory.Triangulated.TStructure.Heart.full_ι._autoParam} →
                              {faithful_ι :
                                  autoParam ι.Faithful
                                    CategoryTheory.Triangulated.TStructure.Heart.faithful_ι._autoParam} →
                                {essImage_eq_heart :
                                    autoParam (ι.essImage = t.heart)
                                      CategoryTheory.Triangulated.TStructure.Heart.essImage_eq_heart._autoParam} →
                                  {ι' : CategoryTheory.Functor H C} →
                                    {additive_ι' :
                                        autoParam ι'.Additive
                                          CategoryTheory.Triangulated.TStructure.Heart.additive_ι._autoParam} →
                                      {full_ι' :
                                          autoParam ι'.Full
                                            CategoryTheory.Triangulated.TStructure.Heart.full_ι._autoParam} →
                                        {faithful_ι' :
                                            autoParam ι'.Faithful
                                              CategoryTheory.Triangulated.TStructure.Heart.faithful_ι._autoParam} →
                                          {essImage_eq_heart' :
                                              autoParam (ι'.essImage = t.heart)
                                                CategoryTheory.Triangulated.TStructure.Heart.essImage_eq_heart._autoParam} →
                                            { ι := ι, additive_ι := additive_ι, full_ι := full_ι,
                                                  faithful_ι := faithful_ι, essImage_eq_heart := essImage_eq_heart } =
                                                { ι := ι', additive_ι := additive_ι', full_ι := full_ι',
                                                  faithful_ι := faithful_ι', essImage_eq_heart := essImage_eq_heart' } →
                                              (ι ≍ ι' → P) → P