Commit 2025-10-10 06:53 029f3b68

refactor: weaken HasPullbacks to HasPullback in Over.Pullback (#29795) Add an abbreviation HasPullbackAlong f to mean that all maps into the codomain of f have pullbacks along f. As discussed in zulip #mathlib4 > Hom.HasPullback The HasPullbacks instance on a category C for defining the pullback functor along a map f : X -> Y between their over categories can be weakened to just a HasPullbackAlong condition on f. Dually, for HasPushout and undercategories.