∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {W : CategoryTheory.MorphismProperty C} {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D] {F₁ F₂ : CategoryTheory.Functor W.Localization D}
  (τ : W.Q.comp F₁ ⟶ W.Q.comp F₂) ⦃X Y : W.Localization⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (F₁.map f) (CategoryTheory.Localization.Construction.NatTransExtension.app τ Y) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.NatTransExtension.app τ X) (F₂.map f)