Definition SS_disp_monoidal_data : disp_monoidal_data SS_disp_cat SET_cart_monoidal. Proof. exists (SS_disp_cat_tensor). exists (totalsubtype (pr1 unitHSET)). repeat (use tpair). - intros X U x xinU_prop. use (factor_through_squash _ _ xinU_prop). { apply U. } intro xinU. rewrite (! pr12 xinU). exact (pr222 xinU). - intros X U x xinU_prop. exists tt. use (factor_through_squash _ _ xinU_prop). { apply U. } intro xinU. rewrite (! pr12 xinU). exact (pr22 xinU). - intros X U x xinU_prop. use (factor_through_squash _ _ xinU_prop). { apply U. } intro xinU. rewrite (! pr12 xinU). exact (pr122 xinU). - intros X U x xinU_prop. refine (_ ,, tt). use (factor_through_squash _ _ xinU_prop). { apply U. } intro xinU. rewrite (! pr12 xinU). exact (pr22 xinU). - intros X Y Z U V W xyz xyzinUVW_prop. use (factor_through_squash _ _ xyzinUVW_prop). { repeat (apply isapropdirprod). + apply U. + apply V. + apply W. } intro xyzinUVW. rewrite (! pr12 xyzinUVW). repeat split ; apply (pr22 xyzinUVW). - intros X Y Z U V W xyz xyzinUVW_prop. use (factor_through_squash _ _ xyzinUVW_prop). { repeat (apply isapropdirprod). + apply U. + apply V. + apply W. } intro xyzinUVW. rewrite (! pr12 xyzinUVW). repeat split ; apply (pr22 xyzinUVW). 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.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.MonoidalSections. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian. Require Import UniMath.CategoryTheory.Monoidal.Examples.SetCartesianMonoidal.