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

Add definitions for preservation/reflection of specific (co)limits #82

Open
TOTBWF opened this issue May 17, 2022 · 1 comment
Open
Labels
category-theory For issues/pull requests relating to the Cat.* namespace enhancement New feature or request

Comments

@TOTBWF
Copy link
Collaborator

TOTBWF commented May 17, 2022

Right now we have a notion of preservation/reflection of (co)limits that works over limit diagrams, but this is often a bit annoying to work with when we are working with some concrete (co)limit, as it involves dancing between limit diagrams + the concrete definitions. It would be a bit more ergonomic if we had some definitions like Preserves-products or Reflects-coequalisers, as well as a good API for moving between the general + specific forms.

@TOTBWF TOTBWF added enhancement New feature or request category-theory For issues/pull requests relating to the Cat.* namespace labels May 17, 2022
@plt-amy
Copy link
Member

plt-amy commented May 17, 2022

Note that this would involve refactoring the definition of is-lex in Cat.Diagrams.Limit.Finite to use the new predicates.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
category-theory For issues/pull requests relating to the Cat.* namespace enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

2 participants