Lemma disp_tensor_with_id_on_right {C : category} {D : disp_cat C} {M : monoidal C} {DM : disp_monoidal D M} {x y z : C} {f : C⟦x, y⟧} {xx : D x} {yy : D y} {zz : D z} (ff : xx -->[f] yy) : ff ⊗⊗^{ DM} id_disp zz = transportb _ (when_bifunctor_becomes_rightwhiskering M z f) (ff ⊗⊗^{ DM}_{r} zz). Proof. unfold dispfunctoronmorphisms1. etrans. { apply maponpaths. apply disp_bifunctor_leftid. } etrans. { apply mor_disp_transportf_prewhisker. } use transportf_transpose_left. rewrite transport_b_b. etrans. { apply id_right_disp. } apply maponpaths_2. apply homset_property. 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Import BifunctorNotations. Import MonoidalNotations. Import DisplayedBifunctorNotations. Import DisplayedMonoidalNotations.