[Merged by Bors] - feat(CategoryTheory/Limits/Shapes/Biproducts): add associator #7127
Conversation
eric-wieser
added
awaiting-review
eric-wieser
force-pushed
the
eric-wieser/biprod-associator
branch
from
24b9f50
to
dc9ef57
Compare
eric-wieser
force-pushed
the
eric-wieser/biprod-associator
branch
from
6ee8fc0
to
7cdf318
Compare
|
|
||
| /-- The associator isomorphism can be passed through a map by swapping the order. -/ | ||
| @[reassoc] | ||
| theorem biprod.associator_natural {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) : |
There was a problem hiding this comment.
biprod.associator_hom_naturality might be a slightly better name; and biprod.associator_inv_natural(ity) also.
There was a problem hiding this comment.
This name was copied from biprod.braid_natural above. Would you like me to rename both, or are you happy for me to leave things as is?
There was a problem hiding this comment.
Ah ok. Then, it is ok to leave it as is.
|
bors d+ |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
and removed
awaiting-review
|
bors merge |
As far as I can tell this doesn't exist anywhere else. The motivation is #7125, but I have a lot less idea of what I'm doing there than I do here.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
As far as I can tell this doesn't exist anywhere else. The motivation is #7125, but I have a lot less idea of what I'm doing there than I do here.
As far as I can tell this doesn't exist anywhere else. The motivation is #7125, but I have a lot less idea of what I'm doing there than I do here.