Open
Description
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 inCategories.Diagram.Pullbackand one inCategories.Diagram.Pullback.Properties unique′,id-unique, andunique-diagramare treated as properties for pushouts and exported byCategories.Diagram.Pushout.Properties, whereas they are treated as conservative extensions (i.e. record fields) for pullbacks and exported byCategories.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.
Metadata
Metadata
Assignees
Labels
No labels