∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} (X : C),
  CategoryTheory.Localization.Construction.relations W
    (CategoryTheory.Localization.Construction.ψ₁ W (CategoryTheory.CategoryStruct.id X))
    (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W X))