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.
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.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.Initial. Require Import UniMath.Bicategories.Core.Examples.Final. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.CleavingOfBicat. Require Import UniMath.Bicategories.DisplayedBicats.FiberCategory. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Import PseudoFunctor.Notations.