Commit 2024-10-12 12:46 a02b71d0

feat(MorphismProperty/Presheaf): add relative morphism property (#16143) Given a morphism property P and a functor F, we define the morphism property P.relative of morphisms in the codomain of F. This is defined as being relatively representable with respect to F, and that any represented pullback of the morphism satisfies P.