Commit 2024-07-18 10:47 3f9dc4a1

View on Github →

chore(CategoryTheory/Monoidal): oplax functors and comonoids (#13312) Oplax monoidal functors take comonoids to comonoids. Also, generalize constructions of limits in Mon_ so limits of a particular shape in C are enough to give limits of that shape in Mon_ C.

depends on: #13310
depends on: #13316

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/FunctorCategory.lean

added def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso

added def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor

added def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj

added def CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj

deleted def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Functor.obj

deleted def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.Inverse.obj

added def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj

added def CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj

added def CategoryTheory.Monoidal.comonFunctorCategoryEquivalence

Modified Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

Modified Mathlib/CategoryTheory/Monoidal/Limits.lean

Created test/CategoryTheory/Mon_.lean