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 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-α→

_ = Deloop


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.