proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.Monoidal.Displayed.Monoidal