Commit 2022-08-24 09:35 912a310a

refactor(category_theory/morphism_property): stable_under_base_change (#16196) This PR redefines morphism_property.stable_under_base_change P. This condition now states that for all pullback squares (is_pullback), the left map satisfies the property if the right map does. Then, it is automatic that the property P respects isos. A constructor is provided to take as an input the assumption that P respects isos and the previous condition that if a map g satisfies P, then pullback.fst : pullback f g → _ satisfies it P.