Monoidal equivalence and monoidal quasi-inverse data

A monoidal equivalence from $\mathcal{C}$ to $\mathcal{D}$ is a strong monoidal functor $F:\mathcal{C}\to \mathcal{D}$ (Lax, strong, and strict monoidal functors) together with:

• a strong monoidal functor $G:\mathcal{D}\to \mathcal{C}$;
• monoidal natural isomorphisms $\eta :1_{\mathcal{C}}\Rightarrow GF,\epsilon :FG\Rightarrow 1_{\mathcal{D}}$ (Monoidal natural transformation).

Here $GF$ and $FG$ carry the composite strong monoidal structures of Lax monoidal functors compose, and composition preserves strength and strictness, and each identity functor carries the strict monoidal structure whose binary and unit maps are identities. Thus both displayed transformations are between specified lax monoidal functors.

Thus the underlying functor $F$ is an equivalence of categories in the sense of Equivalence, quasi-inverse, and adjoint equivalence of categories, but the monoidal quasi-inverse $G$ is part of the data and not a canonical construction. By Every equivalence of categories can be equipped as an adjoint equivalence, one may choose the underlying equivalence data so that the triangle identities also hold, but that extra choice is not built into the base definition here.