Functor triangle and pentagon

At @spitters' request.  The trick was `equiv_path_path_functor_uncurried`, classifying the type `@paths
(@paths (Functor C D))` as being fully determined by the action on objects.

Also, rename `path_functor'_sig` into `path_functor_uncurried` for consistency with HoTT core.

There's a less automated version in the first commit; once I automated the triangle, the same tactic took care of the pentagon without any changes.