fact: Definition disp_psfunctor_comp {x y z : B₁} {f : x --> y} {g : y --> z} {xx : D₁ x} {yy : D₁ y} {zz : D₁ z} (ff : xx -->[f] yy) (gg : yy -->[g] zz) : disp_invertible_2cell (psfunctor_comp F f g) (comp_disp (disp_psfunctor_mor ff) (disp_psfunctor_mor gg)) (disp_psfunctor_mor (comp_disp ff gg)) := pr222 (pr2 FFdata) x y z f g xx yy zz ff gg.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.Initial UniMath.Bicategories.Core.Examples.Final UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.CleavingOfBicat UniMath.Bicategories.DisplayedBicats.FiberCategory UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.Identity UniMath.Bicategories.PseudoFunctors.Examples.Composition