Definition dirprod_disp_cat_monoidal_data : disp_monoidal_data (dirprod_disp_cat D D') M. Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _ ,, _). - exact dirprod_disp_tensor. - exact (dI_{DM} ,, dI_{D'M}). - intros x [x1 x2]. exact (dlu^{DM} _ x1 ,, dlu^{D'M} _ x2). - intros x [x1 x2]. exact (dluinv^{DM} _ x1 ,, dluinv^{D'M} _ x2). - intros x [x1 x2]. exact (dru^{DM} _ x1 ,, dru^{D'M} _ x2). - intros x [x1 x2]. exact (druinv^{DM} _ x1 ,, druinv^{D'M} _ x2). - intros x y z [x1 x2] [y1 y2] [z1 z2]. exact (dα^{DM} _ _ _ x1 y1 z1 ,, dα^{D'M} _ _ _ x2 y2 z2). - intros x y z [x1 x2] [y1 y2] [z1 z2]. exact (dαinv^{DM} _ _ _ x1 y1 z1 ,, dαinv^{D'M} _ _ _ x2 y2 z2). 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.