Definition dirprod_disp_tensor : disp_bifunctor M (D × D') (D × D') (D × D'). Proof. simple refine ((_ ,, (_,,_)) ,, _). - intros x y xx yy. exact (pr1 xx ⊗⊗_{DM} pr1 yy ,, pr2 xx ⊗⊗_{D'M} pr2 yy). - intros x y1 y2 g xx yy1 yy2 gg. exact (pr1 xx ⊗⊗^{DM}_{l} pr1 gg ,, pr2 xx ⊗⊗^{D'M}_{l} pr2 gg). - intros y1 y2 x f yy1 yy2 xx ff. exact (pr1 ff ⊗⊗^{DM}_{r} pr1 xx ,, pr2 ff ⊗⊗^{D'M}_{r} pr2 xx). - abstract (repeat split ; (try (intro ; intros) ; use total2_paths_f ; [apply D_prop | apply D'_prop])). 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Sigma. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Import BifunctorNotations. 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.TotalMonoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Examples.Fullsub. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import MonoidalNotations. Import DisplayedBifunctorNotations. Import DisplayedMonoidalNotations.