Lemma DCM_triangle_identity : disp_triangle_identity DCM_leftunitor_data DCM_rightunitor_data DCM_associator_data. Proof. red; intros. cbn. unfold DCM_associator_data. rewrite dispPostcompWithBinProductArrow. apply pathsinv0, transportf_comp_lemma. apply dispBinProductArrowUnique. - etrans; [apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. etrans; [| apply pathsinv0, dispBinProductOfArrowsPr1]. unfold DCM_rightunitor_data. rewrite assoc_disp_var. rewrite id_right_disp. rewrite transport_f_f. apply pathsinv0, transportf_comp_lemma. etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker]. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - etrans; [apply mor_disp_transportf_postwhisker |]. apply pathsinv0, transportf_comp_lemma. etrans; [| apply pathsinv0, dispBinProductOfArrowsPr2]. rewrite id_right_disp. unfold DCM_leftunitor_data. apply pathsinv0, transportf_comp_lemma. rewrite dispBinProductPr2Commutes. rewrite transport_f_b. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. Qed.
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.