Commit 2024-01-25 06:29 2e59248d
View on Github →refactor(CategoryTheory/Monoidal): split the naturality condition of monoidal functors (#9988)
Extracted from #6307. We replace μ_natural with μ_natural_left and μ_natural_right since we prefer to use the whiskerings to the tensor of morphisms in the refactor #6307.