Definition DCM_tensor_data : disp_bifunctor_data M D D D. Proof. use make_disp_bifunctor_data. - intros c d cc dd. exact (dispBinProductObject D (CP c d) (dP c d cc dd)). - intros c d1 d2 g cc dd1 dd2 gg. exact (dispBinProductOfArrows _ _ _ (id_disp cc) gg). - intros c1 c2 d f cc1 cc2 dd ff. exact (dispBinProductOfArrows _ _ _ ff (id_disp dd)). 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.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Binproducts. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal. Import BifunctorNotations. Import MonoidalNotations. Import DisplayedBifunctorNotations.