Commit 2022-10-01 11:17 8150c5eb
View on Github →feat(category_theory/morphism_property): miscellaneous basic results (#16444)
This PR establishes miscellaneous results about morphism_property in category theory: how stable_under_composition, etc, behave with passing to the opposite category, the definition of the inverse image of a morphism_property by a functor, the definition of isomorphisms/monomorphisms/epimorphisms as morphism properties.