∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (f : CategoryTheory.Arrow C)
  [∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] (n : ℕ),
  CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom