search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
362 stars 68 forks source link

Extremal Morphisms #340

Closed TOTBWF closed 2 years ago

TOTBWF commented 2 years ago

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 commented 2 years ago

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 commented 2 years ago

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 :)