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)).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map1Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.Map2Cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictIdentitor. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictCompositor. Require Import UniMath.Bicategories.PseudoFunctors.Display.StrictPseudoFunctorBicat.