Commit 2024-09-12 19:09 9c097105

feat(Tactic/CategoryTheory/ToApp): Add to_app attribute (#16119) This PR adds the attribute to_app, which generates new declarations similar to how reassoc works. The point is the following: given a lemma about an equality of 2-morphisms in some bicategory, to_app specializes this lemma so that the equality is taking place in Cat, then it applies NatTrans.congr_app and simplifies the resulting expression. Lemmas of this form are useful to apply when working with a (simplified) expression of 1-morphisms in a category where parts (but not all) of this expression consists of components of natural transformations. So this attribute makes it easier to apply purely bicategorical lemmas in such situations. A situation where I think that this is useful is when working with pseudofunctors valued in Cat. See the branch bicategory-grothendieck-functoriality for an example of where these automatically generated declarations are used. I think it might also be useful for 2-yoneda, as the pseudofunctors there are valued in Cat also. Much of the code has been copied from reassoc. However, a new definition toCatExpr is added to specialize the lemma so that the equality is taking place in Cat. One also needs some amount of extra preprocessing to properly deal with universes (since Cat has a different dependence on universes than an arbitrary bicategory).