proposition: Lemma DCM_leftunitor_law : disp_leftunitor_law DCM_leftunitor_data DCM_leftunitorinv_data.
proof: Proof. split; [| split]; try red; intros. - cbn. etrans. { apply dispBinProductOfArrowsPr2. } unfold DCM_leftunitor_data. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - cbn. unfold DCM_leftunitorinv_data, DCM_leftunitor_data. rewrite dispBinProductPr2Commutes. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - cbn. unfold DCM_leftunitorinv_data, DCM_leftunitor_data. apply pathsinv0. etrans. 2: { simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). shelve. + apply dispTerminalArrowEq. + shelve. + rewrite assoc_disp_var. rewrite dispBinProductPr2Commutes. apply pathsinv0, transportf_comp_lemma. etrans; [| apply pathsinv0, mor_disp_transportf_prewhisker]. rewrite id_right_disp. rewrite transport_f_b. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. Unshelve. rewrite <- assoc. rewrite BinProductPr2Commutes. apply id_right. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Binproducts UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Examples.CartesianMonoidal