proposition: Lemma pseudofunctor_of_functor__composition_of {x0 x1 x2 x : PreCategory} {x7 x11 : Functor x0 x1} {x12 : x7 = x11} {x6 : Functor x0 x2} {x9 : Functor x2 x1} {x14 : x11 = (x9 o x6)%functor} {x4 : Functor x0 x} {x5 : Functor x x1} {x8 : x7 = (x5 o x4)%functor} {x10 : Functor x x2} {x13 : x6 = (x10 o x4)%functor} {x15 : x5 = (x9 o x10)%functor} (H0' : P x0) (H1' : P x1) (H2' : P x2) (H' : P x) : ((associator_1 x9 x10 x4) o ((idtoiso (x -> x1) x15 : morphism _ _ _) oR x4 o (idtoiso (x0 -> x1) x8 : morphism _ _ _)))%natural_transformation = (x9 oL (idtoiso (x0 -> x2) x13 : morphism _ _ _) o ((idtoiso (x0 -> x1) x14 : morphism _ _ _) o (idtoiso (x0 -> x1) x12 : morphism _ _ _)))%natural_transformation.
proof: Proof. clear F. symmetry; simpl; pseudofunctor_t. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws Functor.Identity Pseudofunctor.Core Cat.Core FunctorCategory.Core FunctorCategory.Morphisms NaturalTransformation.Isomorphisms Category.Morphisms NaturalTransformation.Paths Basics.PathGroupoids Basics.Trunc