∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) [P.RespectsIso]
  {X Y : C} (g : X ⟶ Y),
  (∀ {T : C} (f : T ⟶ Y) [inst_2 : CategoryTheory.Limits.HasPullback f g], P (CategoryTheory.Limits.pullback.fst f g)) →
    P.universally g