proposition: Lemma triangle 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: Proof. coherence_t. Qed.
imports: Category.Core Functor.Core Functor.Composition.Core Functor.Identity Functor.Paths Basics.PathGroupoids Basics.Tactics