Definition DCM_associator_data : disp_associator_data DCM_tensor. Proof. red; intros. apply dispBinProductArrow. + use comp_disp. 2: {apply dispBinProductPr1. } apply dispBinProductPr1. + apply dispBinProductArrow. * use comp_disp. 2: {apply dispBinProductPr1. } apply dispBinProductPr2. * apply dispBinProductPr2. 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.