-
Notifications
You must be signed in to change notification settings - Fork 251
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: basic definition of comonoid objects #10091
Conversation
semorrison
commented
Jan 29, 2024
rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc] | ||
|
||
theorem assoc_flip : | ||
M.comul ≫ (𝟙 M.X ⊗ M.comul) = M.comul ≫ (M.comul ⊗ 𝟙 M.X) ≫ (α_ M.X M.X M.X).hom := by simp |
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'm not familiar with the current setup for monoidal categories. It looks to me that neither LHS nor the RHS of this lemma are in simp-normal form due to the simp lemmas id_tensorHom
and tensorHom_id
. Should the statement be changed? Why doesn't the simpNF linter complain about 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.
simpNF
doesn't complain because this isn't a simp lemma!
I fixed this to use whiskering.
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've actually now changed both the associativity lemmas, to absorb associators, and made both simp. Probably this will break the downstream PRs, whose content I've entirely forgotten by now. :-)
Thanks! bors merge |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net>
Pull request successfully merged into master. Build succeeded: |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net>