proposition: Lemma disp_functor_ff_inv_compose {x y z : C} {f : x --> y} {g : y --> z} {xx} {yy} {zz} (ff : FF _ xx -->[#F f] FF _ yy) (gg : FF _ yy -->[#F g] FF _ zz) : disp_functor_ff_inv (transportb _ (functor_comp F _ _ ) (ff ;; gg)) = disp_functor_ff_inv ff ;; disp_functor_ff_inv gg.
proof: Proof. apply invmap_eq. cbn. apply pathsinv0. etrans. apply (disp_functor_comp FF). apply maponpaths. etrans. apply maponpaths. exact (homotweqinvweq _ _). apply maponpaths_2. exact (homotweqinvweq _ _). Qed.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos