-
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/bicategory/coherence_tactic): coherence tactic for bicategories #13417
Conversation
This looks great, sorry about the delay. (With the merge conflict it had dropped off my radar. Please feel free to mention PRs that haven't seen any action in a week on zulip. :-) bors merge |
…or bicategories (#13417) This PR extends the coherence tactic for monoidal categories #13125 to bicategories. The setup is the same as for monoidal case except for the following : we normalize 2-morphisms before running the coherence tactic. This normalization is achieved by the set of simp lemmas in `whisker_simps` defined in `coherence_tactic.lean`. As a test of the tactic in the real world, I have proved several properties of adjunction in bicategories in #13418. Unfortunately some proofs cause timeout, so it seems that we need to speed up the coherence tactic in the future. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
The build failed, unfortunately. Please fix and put back on the queue, thanks! |
✌️ yuma-mizuno can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…or bicategories (#13417) This PR extends the coherence tactic for monoidal categories #13125 to bicategories. The setup is the same as for monoidal case except for the following : we normalize 2-morphisms before running the coherence tactic. This normalization is achieved by the set of simp lemmas in `whisker_simps` defined in `coherence_tactic.lean`. As a test of the tactic in the real world, I have proved several properties of adjunction in bicategories in #13418. Unfortunately some proofs cause timeout, so it seems that we need to speed up the coherence tactic in the future. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This needs to be added to Mathport/Syntax.lean in mathlib4. |
Should have been added after leanprover-community/mathlib#13417. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Should have been added after leanprover-community/mathlib#13417. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This PR extends the coherence tactic for monoidal categories #13125 to bicategories. The setup is the same as for monoidal case except for the following : we normalize 2-morphisms before running the coherence tactic. This normalization is achieved by the set of simp lemmas in
whisker_simps
defined incoherence_tactic.lean
.As a test of the tactic in the real world, I have proved several properties of adjunction in bicategories in #13418. Unfortunately some proofs cause timeout, so it seems that we need to speed up the coherence tactic in the future.