C D E (F : Functor C D) (G : Functor D E) : (associativity F 1 G @ ap (compose G) (left_identity F)) = (ap (fun G' : Functor D E => G' o F) (right_identity G)). 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.