(F : Functor C D) : 1 o F = 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.