fact: Record PseudonaturalTransformation `{Funext} (X : PreCategory) (F G : Pseudofunctor X) := { p_components_of :> forall a : X, Functor (F a) (G a); p_commutes : forall (x y : X) (m : morphism X x y), ((p_components_of y o p_morphism_of F m)%functor <~=~> (p_morphism_of G m o p_components_of x)%functor)%natural_transformation; p_commutes_respects_identity : forall x : X, ((left_identity_natural_transformation_1 (p_components_of x)) o (p_identity_of G x oR p_components_of x) o (p_commutes x x 1%morphism) o (p_components_of x oL (p_identity_of F x) ^-1) o (right_identity_natural_transformation_2 (p_components_of x)) = 1)%natural_transformation; p_commutes_respects_composition : forall (x y z : X) (m1 : morphism X y z) (m2 : morphism X x y), (((associator_2 (p_morphism_of G m1) (p_morphism_of G m2) (p_components_of x)) o (p_morphism_of G m1 oL p_commutes x y m2) o (associator_1 (p_morphism_of G m1) (p_components_of y) (p_morphism_of F m2)) o (p_commutes y z m1 oR p_morphism_of F m2) o (associator_2 (p_components_of z) (p_morphism_of F m1) (p_morphism_of F m2))) = ((p_composition_of G x y z m1 m2 oR p_components_of x o p_commutes x z (m1 o m2)%morphism) o (p_components_of z oL (p_composition_of F x y z m1 m2) ^-1)))%natural_transformation }.
imports: Category.Core Functor.Core NaturalTransformation.Core Pseudofunctor.Core Category.Morphisms FunctorCategory.Morphisms Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws NaturalTransformation.Identity