Lemma cancel_precomposition_disp {C} {D : disp_cat C} {x y z} {f : x --> y} {g g' : y --> z} {e : g' = g} {xx : D x} {yy} {zz} (ff : xx -->[f] yy) {gg : yy -->[g] zz} {gg' : yy -->[g'] zz} (ee : gg = transportf _ e gg') : ff ;; gg = transportf _ (cancel_precomposition _ _ _ _ _ _ f e) (ff ;; gg'). Proof. etrans. apply maponpaths, ee. apply mor_disp_transportf_prewhisker. Qed.
Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.AxiomOfChoice. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering.