Library asymmetry in Categories.Diagram.*

[jacquescomeaux]

Hi, thanks for this excellent library.

I needed an up-to-iso for pushouts and noticed that is was missing, even though the dual theorem is available for pullbacks.

This led me to notice some other pullback/pushout quirks and inconsistencies. For example:

• There are two versions of pullback-resp-≈, one in Categories.Diagram.Pullback and one in Categories.Diagram.Pullback.Properties
• unique′, id-unique, and unique-diagram are treated as properties for pushouts and exported by Categories.Diagram.Pushout.Properties, whereas they are treated as conservative extensions (i.e. record fields) for pullbacks and exported by Categories.Diagram.Pullback
• Pullbacks come in bundled and unbundled form, while pushouts only come bundled

I'd like to make things consistent between pullbacks and pushouts, and a cursory look at the other modules in Categories.Diagram.* suggests that a few of the other Thing / Cothing pairs could benefit from a similar cleanup.

[JacquesCarette]

All of these are typical warts of libraries that grow organically. Thanks for noticing and listing them explicitly.

A bunch of small PRs fixing this would be most welcome. Definitely best to do it piece-by-piece, so that the uncontroversial stuff can just go in, and anything that needs discussion doesn't hold anything up.

For some of these, it might be wise to first open an issue, to discuss which way we'd like to resolve the inconsistency. That way you won't waste your time implementing a solution that goes in the opposite direction of expectations. But each one of these inconsistencies should get fixed.