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): connected components of a category #5425
Conversation
b-mehta
commented
Dec 18, 2020
•
edited by github-actions
bot
edited by github-actions
bot
- depends on: [Merged by Bors] - feat(data/list/chain): chain pmap #5438
- depends on: [Merged by Bors] - feat(data/list/chain): relate chain to refl trans gen #5437
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
category structure. | ||
This category is equivalent to `J`. | ||
-/ | ||
abbreviation decomposed (J : Type u₁) [category.{v₁} J] := |
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.
This name seems somewhat generic, and it's in the category_theory
namespace.
Same holds for inclusion
below it, which is even more generic, maybe.
Maybe they should be namespaced?
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.
Sounds like a good idea - or just picking a more descriptive name for these. Do you have suggestions?
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.
I couldn't really come up with a good name for this one... you could ask on Zulip, maybe someone has inspiration
Is this PR all good other than the naming question above? |
Yes, sorry, I lost track of this PR. It adds @b-mehta If you want to change it, go ahead. Otherwise, let's just merge this. Thanks for the PR! bors d+ |
✌️ b-mehta can now approve this pull request. To approve and merge a pull request, simply reply with |
Oh I forgot about this as well! I feel like the name |
@b-mehta ping? |
Oops, I forgot about this too! I've added the comment I mentioned |
bors r+ |
Pull request successfully merged into master. Build succeeded: |