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