{P : Sort u} →
  {C₁ : Type u_1} →
    {C₂ : Type u_2} →
      {inst : CategoryTheory.Category.{v_1, u_1} C₁} →
        {inst_1 : CategoryTheory.Category.{v_2, u_2} C₂} →
          {W₁ : CategoryTheory.MorphismProperty C₁} →
            {W₂ : CategoryTheory.MorphismProperty C₂} →
              {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
                {X₂ : C₂} →
                  {R R' : Φ.RightResolution X₂} →
                    {t : R.Hom R'} →
                      {C₁' : Type u_1} →
                        {C₂' : Type u_2} →
                          {inst' : CategoryTheory.Category.{v_1, u_1} C₁'} →
                            {inst'_1 : CategoryTheory.Category.{v_2, u_2} C₂'} →
                              {W₁' : CategoryTheory.MorphismProperty C₁'} →
                                {W₂' : CategoryTheory.MorphismProperty C₂'} →
                                  {Φ' : CategoryTheory.LocalizerMorphism W₁' W₂'} →
                                    {X₂' : C₂'} →
                                      {R'_1 R'' : Φ'.RightResolution X₂'} →
                                        {t' : R'_1.Hom R''} →
                                          C₁ = C₁' →
                                            C₂ = C₂' →
                                              inst ≍ inst' →
                                                inst_1 ≍ inst'_1 →
                                                  W₁ ≍ W₁' →
                                                    W₂ ≍ W₂' →
                                                      Φ ≍ Φ' →
                                                        X₂ ≍ X₂' →
                                                          R ≍ R'_1 →
                                                            R' ≍ R'' →
                                                              t ≍ t' →
                                                                CategoryTheory.LocalizerMorphism.RightResolution.Hom.noConfusionType
                                                                  P t t'