Commit 2024-10-23 16:51 9f64b5d9
View on Github →feat(CategoryTheory/ChosenFiniteProducts): Monoidal functors between categories with chosen products (#17613)
Introduce a counterpart of Functor.toMonoidalFunctorOfHasFiniteProducts for categories with chosen finite products.