agda-categories
agda-categories copied to clipboard
Revisit location of certain canonical instances
@sergey-goncharov mentionned:
So, my logic was: you have canonical pullbacks in Categories.Category.Instance.Properties.Setoids.Limits.Canonical and pullbacks are only special limits, so, I though I should put binary coproducts, which are special colimits to Categories.Category.Instance.Properties.Setoids.Colimits.Canonical
That logic is sound - but I think the idea of putting pullback in limits is counter to findability. I would not have looked there. Not because I don't know that a pullback is a limit, but because the rest of the library doesn't bundle up special cases like this. So this should be split/moved.