Commit 2024-05-15 10:47 a93dd616
View on Github →feat(CategoryTheory/Monoidal): the curried associator isomorphism (#11701)
This PR introduces curriedAssociatorNatIso : bifunctorComp₁₂ (curriedTensor C) (curriedTensor C) ≅ bifunctorComp₂₃ (curriedTensor C) (curriedTensor C) which is a formulation of the associator isomorphism in a monoidal category as an isomorphism between trifunctors C ⥤ C ⥤ C ⥤ C. A little cleanup of the file CategoryTheory.Monoidal.Category is also done.