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. 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.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.