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₂} →
                  {L L' : Φ.LeftResolution X₂} →
                    L.Hom L' →
                      {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₂'} → {L' L'' : Φ'.LeftResolution X₂'} → L'.Hom L'' → Sort u