Transport a monoidal structure along an equivalence. #
When C
and D
are equivalent as categories,
we can transport a monoidal structure on C
along the equivalence,
obtaining a monoidal structure on D
.
We then upgrade the original functor and its inverse to monoidal functors
with respect to the new monoidal structure on D
.
Transport a monoidal structure along an equivalence of (plain) categories.
Instances For
A type synonym for D
, which will carry the transported monoidal structure.
Instances For
We can upgrade e.functor
to a lax monoidal functor from C
to D
with the transported structure.
Instances For
We can upgrade e.functor
to a monoidal functor from C
to D
with the transported structure.
Instances For
We can upgrade e.inverse
to a monoidal functor from D
with the transported structure to C
.
Instances For
The unit isomorphism upgrades to a monoidal isomorphism.
Instances For
The counit isomorphism upgrades to a monoidal isomorphism.