(F : Functor B C) (G : Functor C D) (H : Functor D E) : (H o G) o F = H o (G o F). Proof. by path_functor. Defined.
Require Import Category.Core Functor.Core Functor.Composition.Core Functor.Identity. Require Import Functor.Paths. Require Import Basics.PathGroupoids Basics.Tactics.