Definition cmonoidal_to_noncurriedmonoidal : ob UMONCAT ≃ ∑ C : monoidal_cat, is_univalent (monoidal_cat_cat C). Proof. refine (_ ∘ equivalence_cmon_structure_oblayer)%weq. refine (_ ∘ _)%weq. { use weqfibtototal. 2: exact (λ C, cmon_equiv_wmon (pr1 C)). } refine (_ ∘ _)%weq. 1: apply weqtotal2comm12. use weq_subtypes'. - refine (moncats0_equiv_uncurried ∘ moncats_equiv_moncats0 ∘ _)%weq. use weqfibtototal. intro C. exact (invweq (monoidal_struct_equiv_monoidal C)). - intro ; apply isaprop_is_univalent. - intro ; apply isaprop_is_univalent. - intro ; apply isrefl_logeq. 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorCategory. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.EquivalenceWhiskeredNonCurriedMonoidalCategories. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.AssociatorUnitorsLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.FinalLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.AssociatorUnitorsLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.FinalLayer. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.EquivalenceMonCatCurried. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.EquivalenceWhiskeredCurried.