Lemma moncats_equiv_moncats0 : moncats ≃ moncats0. Proof. apply weqfibtototal. intro C. unfold monoidal_struct ; unfold monstruct0. use weq_iso. - intro M. exists (pr111 M). exists (pr211 M). repeat (use tpair). * intro x ; apply (pr1 (pr121 M) x). * intros x y f ; apply (pr2 (pr121 M) x y f). * intro x ; apply (pr1 (pr122 M) x). * intro x ; apply (pr2 (pr122 M) x). * intro x ; apply (pr11 (pr221 M) x). * intros x y f ; apply (pr21 (pr221 M) x y f). * intro x ; apply (pr11 (pr222 M) x). * intro x ; apply (pr21 (pr222 M) x). * intros x y z ; apply (pr12 (pr221 M) x y z). * intro ; intros ; apply (pr122 (pr221 M)). * intro ; intros ; apply (pr1 (pr222 (pr221 M))). * intro ; intros ; apply (pr2 (pr222 (pr221 M))). * intro ; intros ; apply ((pr12 (pr222 M))). * intro ; intros ; apply ((pr22 (pr222 M))). * intro ; intros ; apply (pr112 M). * intro ; intros ; apply (pr212 M). - intro M. use tpair. + exists (pr1 M ,, pr12 M). repeat split ; apply (pr22 M). + simpl. repeat split. * apply (pr22 (pr222 M)). * apply (pr22 (pr222 M)). * apply ((pr122 M)). * apply (pr1 (pr222 M)). * apply (pr12 (pr222 M)). - apply idpath. - apply idpath. 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.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered.