Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Revisit location of certain canonical instances #321

Open
JacquesCarette opened this issue Nov 19, 2021 · 0 comments
Open

Revisit location of certain canonical instances #321

JacquesCarette opened this issue Nov 19, 2021 · 0 comments

Comments

@JacquesCarette
Copy link
Collaborator

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant