A B C D E (F : Functor A B) (G : Functor B C) (H : Functor C D) (K : Functor D E) : (associativity F G (K o H) @ associativity (G o F) H K) = (ap (fun KHG => KHG o F) (associativity G H K) @ associativity F (H o G) K @ ap (compose K) (associativity F G H)). Proof. coherence_t. Qed.
Require Import Category.Core Functor.Core Functor.Composition.Core Functor.Identity. Require Import Functor.Paths. Require Import Basics.PathGroupoids Basics.Tactics.