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
[Merged by Bors] - feat(category_theory/limits/concrete): simp lemmas #3973
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element. This isn't exhaustive; just the things I've wanted recently. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed (retrying...): |
Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element. This isn't exhaustive; just the things I've wanted recently. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
bors d+ |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element. This isn't exhaustive; just the things I've wanted recently. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This PR was included in a batch that was canceled, it will be automatically retried |
@semorrison the build was failing earlier on |
Canceled. |
Trying again after a merge! bors merge |
Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element. This isn't exhaustive; just the things I've wanted recently. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
bors merge |
Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element. This isn't exhaustive; just the things I've wanted recently. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element. This isn't exhaustive; just the things I've wanted recently. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Some specialisations of simp lemmas about (co)limits for concrete categories, where the equation in morphisms has been applied to an element.
This isn't exhaustive; just the things I've wanted recently.