{P : Sort u} →
  {C : Type u_1} →
    {D : Type u_2} →
      {inst : CategoryTheory.Category.{v_1, u_1} C} →
        {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
          {L : CategoryTheory.Functor C D} →
            {W : CategoryTheory.MorphismProperty C} →
              {E : Type u_3} →
                {inst_2 : CategoryTheory.Category.{v_3, u_3} E} →
                  {t : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E} →
                    {C' : Type u_1} →
                      {D' : Type u_2} →
                        {inst' : CategoryTheory.Category.{v_1, u_1} C'} →
                          {inst'_1 : CategoryTheory.Category.{v_2, u_2} D'} →
                            {L' : CategoryTheory.Functor C' D'} →
                              {W' : CategoryTheory.MorphismProperty C'} →
                                {E' : Type u_3} →
                                  {inst'_2 : CategoryTheory.Category.{v_3, u_3} E'} →
                                    {t' : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L' W' E'} →
                                      C = C' →
                                        D = D' →
                                          inst ≍ inst' →
                                            inst_1 ≍ inst'_1 →
                                              L ≍ L' →
                                                W ≍ W' →
                                                  E = E' →
                                                    inst_2 ≍ inst'_2 →
                                                      t ≍ t' →
                                                        CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.noConfusionType
                                                          P t t'