Extremal Morphisms

[TOTBWF]

Patch Description

This PR implements Extremal Morphisms, and proves some properties about them. It also proves some helper lemmas about epis/monos, and performs some minor cleanup of equalizers + coequalizers.

Notes

The names of the morphisms in RegularMono/RegularEpi are really annoying... Perhaps there's a better choice instead of g and h?

[JacquesCarette]

Nice.

A couple of minor things (no need to change for this PR):

• it really is best to use using as much as possible on all open import
• I really would have preferred 2 PRs, one for the clean-up, and one for the new functionality.

[JacquesCarette]

Can you open an issue about the naming of the fields in RegularMono / RegularEpi ? I agree that these names are too short and not meaningful. But I'd like more people to have a chance to comment. Might be good to see what other libraries use for these names (i.e. outside the Agda ecosystem).

[TOTBWF]

Opened #341 to track the naming issue. I'll leave this up for a few days to get feedback, but if no one has anything to say I think we should be good to merge :)