∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X : C} {R : CategoryTheory.Presieve X} {Y : C} (f : Y ⟶ X)
  [self : R.HasPullbacks f] {Z : C} {h : Z ⟶ X}, R h → CategoryTheory.Limits.HasPullback h f