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