proposition: Lemma associativity (F : Functor B C) (G : Functor C D) (H : Functor D E) : (H o G) o F = H o (G o F).
proof: Proof. by path_functor. Defined.
imports: Category.Core Functor.Core Functor.Composition.Core Functor.Identity Functor.Paths Basics.PathGroupoids Basics.Tactics