Definition csmonfunctor_equiv_wsmonfunctor : csmonfunctor ≃ wsmonfunctor. Proof. unfold csmonfunctor ; unfold wsmonfunctor. unfold functor_strong_monoidal ; unfold fmonoidal. use weqtotal2. { apply cmonfunctor_equiv_wmonfunctor. } intro cmf. apply weqimplimpl. - intro csmf. split. + do 2 intro. apply (pr2 csmf). + apply (pr1 csmf). - intro csmf. split. + apply (pr2 csmf). + do 2 intro ; apply (pr1 csmf). - apply isaprop_functor_strong. - apply isapropdirprod ; repeat (apply impred_isaprop ; intro) ; apply Isos.isaprop_is_z_isomorphism. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import BifunctorNotations.