Definition monoidal_swapped_data {V : category} (Mon_V : monoidal V) : monoidal_data V. Proof. exists (tensor_swapped Mon_V). exists I_{Mon_V}. exists (λ v, ru_{Mon_V} v). exists (λ v, ruinv_{Mon_V} v). exists (λ v, lu_{Mon_V} v). exists (λ v, luinv_{Mon_V} v). exists (λ v1 v2 v3, αinv_{Mon_V} v3 v2 v1). exact (λ v1 v2 v3, α_{Mon_V} v3 v2 v1). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful. Require Import UniMath.CategoryTheory.opp_precat. Import BifunctorNotations. Import MonoidalNotations. Section EquivalenceFromTensorWithUnit. Import MonoidalNotations. End EquivalenceFromTensorWithUnit. Import MonoidalNotations. Import MonoidalNotations. Import MonoidalNotations. Import MonoidalNotations. Import MonoidalNotations.