s d d' (m1 : morphism C s d) (m2 : morphism C d d') : c_morphism_of (m2 o m1) = c_morphism_of m2 o c_morphism_of m1 := transport (@paths _ (c_morphism_of (m2 o m1))) (composition_of G _ _ _ _ _) (ap (fun m => G _1 m) (composition_of F _ _ _ m1 m2)).
Require Import Category.Core Functor.Core.