Lemma disp_tensor_distributes_over_transportb_right {C : category} {D : disp_cat C} {M : monoidal C} (DM : disp_monoidal D M) {x y z : C} {f g : y --> z} (p : f = g) (xx : D x) {yy : D y} {zz : D z} (ff : yy -->[f] zz) (gg : yy -->[g] zz) : ff = transportb _ p gg -> xx ⊗⊗^{DM}_{l} transportb _ p ff = transportb _ (maponpaths (leftwhiskering_on_morphisms M x y z) p) (xx ⊗⊗^{DM}_{l} gg). Proof. induction p. intro q. cbn. apply maponpaths. exact q. 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.