Let $C$ be a cartesian closed category. It's well known that $C$ is equivalent to a category where the product is strict monoidal; i.e. where there are equalities of the functors given by the expressions below,
- $1 \times X = X = X \times 1$
- $(X \times Y) \times Z = X \times (Y \times Z)$
Question: Is there a similar coherence theorem including the exponential? E.g. I imagine an internal hom for which there are equalities of functors
- $[1,X] = X$
- $[X \times Y, Z] = [X, [Y,Z]]$
- $[X,1] = 1$
- $[X, Y \times Z] = [X, Y] \times [X, Z]$
Bonus question: Can we further assume that the set of objects, together with the operations, is a free algebra for the variety of universal algebra on the constant $1$, binary operations $\times$ and $[,]$, and satisfying the above axioms and monoid axioms?
I'm also curious about general closed monoidal categories. Obviously we can't ask for all four of these axioms, but can we get the first two?
