agda-stdlib

agda-stdlib copied to clipboard

In Algebra.Morphism.Structures and the similar modules for lattices and modules, we define IsXHomomorphism, IsXMonomorphism, and IsXIsomorphism. We do not currently define IsXEpimorphism, for morphisms that are surjective but not necessarily injective. This feels an obvious omission, and would be useful for defining, for example, projective objects (cf. wp:Projective module)

... And for using the proof that the unique morphism from any Algebra to its corresponding terminal object is StrictlySurjective #2296