Lemma mor_disp_transportb_postwhisker {C : precategory} {D : disp_cat_data C} {x y z : C} {f f' : x --> y} {g : y --> z} (ef : f' = f) {xx : D x} {yy} {zz} (ff' : xx -->[f] yy) (gg : yy -->[g] zz) : (transportb _ ef ff') ;; gg = transportb _ (cancel_postcomposition _ _ g ef) (ff' ;; gg). Proof. destruct ef ; apply idpath. 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Core.Isos. Import BifunctorNotations. Import DisplayedBifunctorNotations.