proposition: Lemma identity_associativity (w x y z : PreCategory) (f : Functor w x) (g : Functor x y) (h : Functor y z) : associator_1 h g f o (1 oR f o 1) = h oL 1 o (1 o @morphism_isomorphic _ _ _ (idtoiso (w -> z) (ap idmap (Functor.Composition.Laws.associativity f g h)))).
proof: Proof. t. Defined.
imports: FunctorCategory.Morphisms Category.Core Functor.Core NaturalTransformation.Isomorphisms NaturalTransformation.Paths Cat.Core Pseudofunctor.Core PathGroupoids