Lemma DCM_rightunitor_law : disp_rightunitor_law DCM_rightunitor_data DCM_rightunitorinv_data. Proof. split; [| split]; try red; intros. - cbn. unfold DCM_rightunitor_data. etrans; [apply dispBinProductOfArrowsPr1 |]. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - cbn. unfold DCM_rightunitorinv_data, DCM_rightunitor_data. rewrite dispBinProductPr1Commutes. apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. - cbn. unfold DCM_rightunitorinv_data, DCM_rightunitor_data. apply pathsinv0. etrans. 2: { simple refine (dispBinProduct_endo_is_identity _ _ _ _ _ _ ?[shH1] _ ?[shH2] _). shelve. + rewrite assoc_disp_var. rewrite dispBinProductPr1Commutes. 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. + shelve. + apply dispTerminalArrowEq. } apply transportf_comp_lemma. apply transportf_comp_lemma_hset; try apply homset_property; apply idpath. Unshelve. rewrite <- assoc. rewrite BinProductPr1Commutes. apply id_right. 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.