proposition: Lemma right_identity (F : Functor C D) : F o 1 = F.
proof: Proof. by path_functor. Defined.
imports: Category.Core Functor.Core Functor.Composition.Core Functor.Identity Functor.Paths Basics.PathGroupoids Basics.Tactics