Port Functor and Category from HoTT-categories

This is the first import from
https://github.com/JasonGross/HoTT-categories.  It contains most of the
precategory and functor basic constructions.  Next up is natural
transformations, but first I want feedback on these.

I tried to cut down on the use of crazy tactics a bit (and found a nicer
proof in Functor.Equality) as a result.  I tried to conform to the
naming conventions of the HoTT library, but I'm not sure I got the order
right in most cases, and would appreciate all feedback (especially
stylistic and organizational feedback).