Transporting a closed monoidal structure along an equivalence of categories #
noncomputable instance
CategoryTheory.MonoidalClosed.instTransported
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
(e : C ≌ D)
[MonoidalCategory C]
[MonoidalClosed C]
:
Equations
- One or more equations did not get rendered due to their size.