fact: Definition is_strict_pstrans {C D : bicat} {F G : strict_psfunctor C D} (η : strict_pstrans_data F G) : UU := (∏ (X Y : C) (f g : X --> Y) (α : f ==> g), (pr1 η X ◃ ##G α) • pr2 η _ _ g = (pr2 η _ _ f) • (##F α ▹ pr1 η Y)) × (∏ (X : C), (pr1 η X ◃ strict_psfunctor_id_cell G X) • pr2 η _ _ (id₁ X) = (runitor (pr1 η X)) • linvunitor (pr1 η X) • (strict_psfunctor_id_cell F X ▹ pr1 η X)) × (∏ (X Y Z : C) (f : X --> Y) (g : Y --> Z), (pr1 η X ◃ strict_psfunctor_comp_cell G f g) • pr2 η _ _ (f · g) = (lassociator (pr1 η X) (#G f) (#G g)) • (pr2 η _ _ f ▹ (#G g)) • rassociator (#F f) (pr1 η Y) (#G g) • (#F f ◃ pr2 η _ _ g) • lassociator (#F f) (#F g) (pr1 η Z) • (strict_psfunctor_comp_cell F f g ▹ pr1 η Z)).
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.DisplayedCats.Core UniMath.CategoryTheory.PrecategoryBinProduct UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.PseudoFunctors.Display.Base UniMath.Bicategories.PseudoFunctors.Display.Map1Cells UniMath.Bicategories.PseudoFunctors.Display.Map2Cells UniMath.Bicategories.PseudoFunctors.Display.StrictIdentitor UniMath.Bicategories.PseudoFunctors.Display.StrictCompositor UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat