(F G : Functor C D) (p q : F = G) : ap object_of p = ap object_of q -> p = q. Proof. refine ((ap (@path_functor_uncurried F G)^-1)^-1 o _). refine ((path_sigma_uncurried _ _ _) o _); simpl. refine (pr1^-1). Defined.
Require Import Category.Core Functor.Core. Require Import HoTT.Basics HoTT.Types HoTT.Tactics.