(F G : Functor C D) (HO : object_of F == object_of G) (HM : forall s d m, transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) (GO d)) (path_forall _ _ HO) (morphism_of F) s d m = G _1 m) : F = G. Proof. refine (path_functor F G (path_forall _ _ HO) _). repeat (apply path_forall; intro); apply HM. Defined.
Require Import Category.Core Functor.Core. Require Import HoTT.Basics HoTT.Types HoTT.Tactics.