-
Notifications
You must be signed in to change notification settings - Fork 297
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): braided and symmetric categories #3550
Conversation
. obviously) | ||
|
||
restate_axiom braided_category.braiding_naturality' | ||
attribute [simp] braided_category.braiding_naturality |
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.
mark these reassoc
too? and make the reassoc
-ed version simp
too, probably
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.
Done!
I also removed simp
from the hexagon identities. We certainly weren't relying on these, and I think it may be better to wait for further applications before deciding on the best simp normal form. Likely we should reverse both hexagon equations, on the principle that the braidings "weigh more" than associators for simp normal form, but I think it's okay to wait here until someone actually wants simp
to apply facts like this.
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.
Ignoring the merge conflict, this looks good to me modulo tiny comments above!
bors merge |
Just the very basics: * the definition of braided and symmetric categories * braided functors, and compositions thereof * the symmetric monoidal structure coming from products * upgrading `Type u` to a symmetric monoidal structure This is prompted by the desire to explore modelling sheaves of modules as the monoidal category of module objects for an internal commutative monoid in sheaves of `Ab`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Just the very basics:
Type u
to a symmetric monoidal structureThis is prompted by the desire to explore modelling sheaves of modules as the monoidal category of module objects for an internal commutative monoid in sheaves of
Ab
.