agda-categories icon indicating copy to clipboard operation
agda-categories copied to clipboard

Revisit location of certain canonical instances

Open JacquesCarette opened this issue 4 years ago • 0 comments

@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.

JacquesCarette avatar Nov 19 '21 15:11 JacquesCarette