module Cat.Monoidal.Reverse {o }
  {C : Precategory o } (Cᵐ : Monoidal-category C)

Reverse monoidal categories🔗

Given a monoidal category with tensor product we can define the reverse monoidal category with the same unit and the tensor product flipped around:

_^rev : Monoidal-category C
_^rev .-⊗- = Flip C.-⊗-
_^rev .Unit = C.Unit

The coherence isomorphisms are straightforward to obtain from those of the left and right unitors are swapped, and the associator is reversed and has its arguments swapped.

_^rev .unitor-l = iso→isoⁿ (isoⁿ→iso C.unitor-r)
  λ f  sym (C.unitor-r .Isoⁿ.to .is-natural _ _ f)
_^rev .unitor-r = iso→isoⁿ (isoⁿ→iso C.unitor-l)
  λ f  sym (C.unitor-l .Isoⁿ.to .is-natural _ _ f)
_^rev .associator = iso→isoⁿ
   (a , b , c)  isoⁿ→iso (C.associator ni⁻¹) (c , b , a))
  λ (f , g , h)  sym (C.associator .Isoⁿ.from .is-natural _ _ (h , g , f))
_^rev .triangle = C.triangle-α→
_^rev .pentagon = C.pentagon-α→

Thinking of monoidal categories as one-object bicategories (via the Delooping construction), the operation corresponds to flipping the 1-cells of a bicategory, leaving the 2-cells unchanged.