fact: Definition psfunctor_lassociator_alt' {B₁ B₂ : bicat} (F : psfunctor B₁ B₂) {a b c d : B₁} (f : a --> b) (g : b --> c) (h : c --> d) : ##F (lassociator f g h) • (psfunctor_comp F _ _)^-1 • ((psfunctor_comp F _ _)^-1 ▹ #F h) • rassociator _ _ _ = (psfunctor_comp F _ _)^-1 • (_ ◃ (psfunctor_comp F _ _)^-1).
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Equivalences.FullyFaithful UniMath.CategoryTheory.DisplayedCats.Core UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.DisplayedBicats.DispBicat 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