Commit 2025-12-03 07:14 14bfbad3

refactor: MorphismProperty.HasPullbacksAlong (#31231) Fix a morphism f : X -> Y in a category C with two morphism properties P and Q. To define a pullback functor between the subcategories of the slice categories P.Over Q Y ⥤ P.Over Q X one does not need the existence of all pullbacks along f. This refactor requires only that f has pullbacks of P-morphisms. This property of "f has pullbacks of P-morphisms is defined as a typeclass. Note that it cannot simply be an abbrev like Limits.HasPullbacksAlong because the typeclass inference system will not be able to infer P that way.