mathlib

0be7214f - feat(category_theory/currying): bifunctor version of whiskering_right (#15504)

feat(category_theory/currying): bifunctor version of whiskering_right (#15504) This cannot go in `category_theory/whiskering` because this file is imported indirectly by `category_theory/functor/currying`. Hopefully it is ok to put it in `category_theory/functor/currying`. - [x] depends on: #15445 Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>