Definition H_strong_monoidal : strong_functor_monoidal_cat lu luD ru ruD α αD. Proof. exists H_monoidal. split. - apply (TransportedTensorComm Duniv H_eso H_ff TC). - apply identity_is_z_iso. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. 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.Core.Univalence. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.catiso. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecompEquivalence. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.TotalCategoryFacts. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.Product. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.FullSubcategory. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensor. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedTensorUnit. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedUnitors. Require Import UniMath.CategoryTheory.Monoidal.RezkCompletion.LiftedAssociator.