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.
Require Import Category.Core Functor.Core Functor.Composition.Core Functor.Identity. Require Import Functor.Paths. Require Import Basics.PathGroupoids Basics.Tactics.