Definition SS_disp_cat_tensor_data : disp_bifunctor_data SET_cart_monoidal SS_disp_cat SS_disp_cat SS_disp_cat. Proof. exists (λ _ _ U V, subtypesdirprod U V). split. - intros X Y1 Y2 g Ux U1 U2 gsp. intros xy2 xy1_prop. use (factor_through_squash _ _ xy1_prop). { apply subtypesdirprod. } intro xy1. split. + rewrite (! pr12 xy1). exact (pr122 xy1). + simpl in *. apply (gsp _). apply hinhpr. exists (pr21 xy1). split. * rewrite (! pr12 xy1). apply idpath. * exact (pr222 xy1). - intros X1 X2 Y f U1 U2 Uy fsp. intros x2y x1y_prop. use (factor_through_squash _ _ x1y_prop). { apply subtypesdirprod. } intro x1y. split. + simpl in *. apply (fsp _). apply hinhpr. exists (pr11 x1y). split. * rewrite (! pr12 x1y). apply idpath. * exact (pr122 x1y). + rewrite (! pr12 x1y). exact (pr222 x1y). 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.