open import Cat.Functor.Naturality
open import Cat.Functor.Bifunctor
open import Cat.Functor.Coherence
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

open Monoidal-category

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

open Cat.Reasoning C
private module C = Monoidal-category Cᵐ
open _=>_

Reverse monoidal categories🔗

Given a monoidal category $C$ with tensor product $\otimes : C \times C \to C,$ we can define the reverse monoidal category $C^{rev}$ with the same unit and the tensor product flipped around: $A \otimes^{rev} B = B \otimes A .$

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

The coherence isomorphisms are straightforward to obtain from those of $C :$ 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-α→

_ = Deloop

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