fact: Definition compose_identity_of x : c_morphism_of (identity x) = identity (c_object_of x) := transport (@paths _ _) (identity_of G _) (ap (fun m => G _1 m) (identity_of F x)).
imports: Category.Core Functor.Core