(F G : Functor C D) (HO : object_of F = object_of G) (HM : transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d)) HO (morphism_of F) = morphism_of G) : F = G := path_functor_uncurried F G (HO; HM).
Require Import Category.Core Functor.Core. Require Import HoTT.Basics HoTT.Types HoTT.Tactics.