fact: Record Pseudofunctor := { p_object_of :> C -> PreCategory; p_morphism_of : forall s d, morphism C s d -> Functor (p_object_of s) (p_object_of d); p_composition_of : forall s d d' (m1 : morphism C d d') (m2 : morphism C s d), (p_morphism_of _ _ (m1 o m2)) <~=~> (p_morphism_of _ _ m1 o p_morphism_of _ _ m2)%functor; p_identity_of : forall x, p_morphism_of x x 1 <~=~> 1%functor; p_composition_of_coherent : forall w x y z (f : morphism C w x) (g : morphism C x y) (h : morphism C y z), ((associator_1 (p_morphism_of y z h) (p_morphism_of x y g) (p_morphism_of w x f)) o ((p_composition_of x y z h g oR p_morphism_of w x f) o (p_composition_of w x z (h o g) f))) = ((p_morphism_of y z h oL p_composition_of w x y g f) o ((p_composition_of w y z h (g o f)) o (Category.Morphisms.idtoiso (_ -> _) (ap (p_morphism_of w z) (Category.Core.associativity C w x y z f g h)) : morphism _ _ _))); p_left_identity_of_coherent : forall x y (f : morphism C x y), ((p_identity_of y oR p_morphism_of x y f) o p_composition_of x y y 1 f) = ((left_identity_natural_transformation_2 (p_morphism_of x y f)) o (Category.Morphisms.idtoiso (_ -> _) (ap (p_morphism_of x y) (Category.Core.left_identity C x y f)) : morphism _ _ _)); p_right_identity_of_coherent : forall x y (f : morphism C x y), ((p_morphism_of x y f oL p_identity_of x) o p_composition_of x x y f 1) = ((right_identity_natural_transformation_2 (p_morphism_of x y f)) o (Category.Morphisms.idtoiso (_ -> _) (ap (p_morphism_of x y) (Category.Core.right_identity C x y f)) : morphism _ _ _)) }.
imports: Category.Core Functor.Core Category.Morphisms FunctorCategory.Morphisms Functor.Composition.Core Functor.Identity NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws FunctorCategory.Core