{P : Sort u} →
  {C : Type u₁} →
    {inst : CategoryTheory.Category.{v₁, u₁} C} →
      {D : Type u₂} →
        {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
          {J : Type w} →
            {inst_2 : CategoryTheory.Category.{w', w} J} →
              {K : CategoryTheory.Functor J C} →
                {F : CategoryTheory.Functor C D} →
                  {t : CategoryTheory.CreatesLimit K F} →
                    {C' : Type u₁} →
                      {inst' : CategoryTheory.Category.{v₁, u₁} C'} →
                        {D' : Type u₂} →
                          {inst'_1 : CategoryTheory.Category.{v₂, u₂} D'} →
                            {J' : Type w} →
                              {inst'_2 : CategoryTheory.Category.{w', w} J'} →
                                {K' : CategoryTheory.Functor J' C'} →
                                  {F' : CategoryTheory.Functor C' D'} →
                                    {t' : CategoryTheory.CreatesLimit K' F'} →
                                      C = C' →
                                        inst ≍ inst' →
                                          D = D' →
                                            inst_1 ≍ inst'_1 →
                                              J = J' →
                                                inst_2 ≍ inst'_2 →
                                                  K ≍ K' →
                                                    F ≍ F' → t ≍ t' → CategoryTheory.CreatesLimit.noConfusionType P t t'