Commit 2022-05-04 05:51 4d0b6301
View on Github →feat(category_theory/bicategory/coherence_tactic): coherence tactic for 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.