{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. clear F. symmetry; simpl; pseudofunctor_t. Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws. Require Import Functor.Identity. Require Import Pseudofunctor.Core. Require Import Cat.Core. Require Import FunctorCategory.Core. Require Import FunctorCategory.Morphisms NaturalTransformation.Isomorphisms. Require Import Category.Morphisms NaturalTransformation.Paths. Require Import Basics.PathGroupoids Basics.Trunc.