fact: Definition equiv_path_functor_uncurried (F G : Functor C D) : path_functor'_T F G <~> F = G := Build_Equiv _ _ (@path_functor_uncurried F G) _.
imports: Category.Core Functor.Core HoTT.Basics HoTT.Types HoTT.Tactics