fact: Definition associativity_fst F G H : ap object_of (associativity F G H) = idpath := @path_functor_uncurried_fst _ _ _ ((H o G) o F) (H o (G o F)) 1%path 1%path.
imports: Category.Core Functor.Core Functor.Composition.Core Functor.Identity Functor.Paths Basics.PathGroupoids Basics.Tactics