Commit 2022-05-04 05:51 4d0b6301

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.