fact: Definition pstrans_comp {C D : bicat} {F G : psfunctor C D} (η : pstrans F G) : ∏ {X Y Z : C} (f : X --> Y) (g : Y --> Z), (η X ◃ psfunctor_comp G f g) • psnaturality_of η (f · g) = (lassociator (η X) (#G f) (#G g)) • (psnaturality_of η f ▹ (#G g)) • rassociator (#F f) (η Y) (#G g) • (#F f ◃ psnaturality_of η g) • lassociator (#F f) (#F g) (η Z) • (psfunctor_comp F f g ▹ η Z) := pr222(pr1 η).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.Examples.Prod UniMath.Bicategories.DisplayedBicats.Examples.FullSub UniMath.Bicategories.PseudoFunctors.Display.Base UniMath.Bicategories.PseudoFunctors.Display.Map1Cells UniMath.Bicategories.PseudoFunctors.Display.Map2Cells UniMath.Bicategories.PseudoFunctors.Display.Identitor UniMath.Bicategories.PseudoFunctors.Display.Compositor UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor