F : ap object_of (right_identity F) = idpath := @path_functor_uncurried_fst _ _ _ (F o 1) F 1 1.
Require Import Category.Core Functor.Core Functor.Composition.Core Functor.Identity. Require Import Functor.Paths. Require Import Basics.PathGroupoids Basics.Tactics.