HoTT/HoTT — pull request #602 by JasonGross (2014-11-01 22:20:27+00:00)
Title: 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.