(F G : Functor C D) : F = G -> path_functor'_T F G := fun H' => (ap object_of H'; (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H')%path.
Require Import Category.Core Functor.Core. Require Import HoTT.Basics HoTT.Types HoTT.Tactics.