Definition precomp_strongmonoidal_catiso : catiso (total_category (functor_strong_monoidal_disp_cat (TransportedLeftUnitor Duniv H_eso H_ff TC I lu) luE (TransportedRightUnitor Duniv H_eso H_ff TC I ru) ruE (TransportedAssociator Duniv H_eso H_ff TC α) αE )) (total_category (functor_strong_monoidal_disp_cat lu luE ru ruE α αE )). Proof. use (adj_equivalence_of_cats_to_cat_iso precomp_strongmonoidal_adj_equiv _ _). - apply is_univalent_StrongMonoidalFunctorCategory. - apply is_univalent_total_category. + apply is_univalent_LaxMonoidalFunctorCategory'. + apply disp_full_sub_univalent. intro ; apply isapropdirprod. * apply NaturalTransformations.isaprop_is_nat_z_iso. * 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.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.