∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C),
  CategoryTheory.Localization.Construction.objEquiv W =
    { toFun := W.Q.obj, invFun := fun X => X.as.obj, left_inv := ⋯, right_inv := ⋯ }