{P : Sort u_1} →
  {C : Type u} →
    {inst : CategoryTheory.Category.{v, u} C} →
      {J : Type w} →
        {inst_1 : LinearOrder J} →
          {inst_2 : OrderBot J} →
            {X Y : C} →
              {f : X ⟶ Y} →
                {inst_3 : SuccOrder J} →
                  {inst_4 : WellFoundedLT J} →
                    {t : CategoryTheory.TransfiniteCompositionOfShape J f} →
                      {C' : Type u} →
                        {inst' : CategoryTheory.Category.{v, u} C'} →
                          {J' : Type w} →
                            {inst'_1 : LinearOrder J'} →
                              {inst'_2 : OrderBot J'} →
                                {X' Y' : C'} →
                                  {f' : X' ⟶ Y'} →
                                    {inst'_3 : SuccOrder J'} →
                                      {inst'_4 : WellFoundedLT J'} →
                                        {t' : CategoryTheory.TransfiniteCompositionOfShape J' f'} →
                                          C = C' →
                                            inst ≍ inst' →
                                              J = J' →
                                                inst_1 ≍ inst'_1 →
                                                  inst_2 ≍ inst'_2 →
                                                    X ≍ X' →
                                                      Y ≍ Y' →
                                                        f ≍ f' →
                                                          inst_3 ≍ inst'_3 →
                                                            inst_4 ≍ inst'_4 →
                                                              t ≍ t' →
                                                                CategoryTheory.TransfiniteCompositionOfShape.noConfusionType
                                                                  P t t'