∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) (L₁ : CategoryTheory.Functor C D₁)
  [inst_3 : L₁.IsLocalization W] (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] {X Y : C},
  CategoryTheory.Localization.homEquiv W L₁ L₂ = CategoryTheory.Localization.homEquiv W_1 L₁ L₂