(F G : Functor C D) : path_functor'_T F G -> F = G. Proof. intros [? ?]. destruct F, G; simpl in *. path_induction; simpl. f_ap; eapply @center; abstract exact _. Defined.
Require Import Category.Core Functor.Core. Require Import HoTT.Basics HoTT.Types HoTT.Tactics.