HoTT/HoTT — pull request #219 by JasonGross (2013-09-27 19:23:04+00:00)
Title: 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).

Any style rules that I got wrong should probably be clarifies at https://github.com/HoTT/HoTT/wiki/Contributing-to-the-HoTT-library#wiki-style, since that's what I based my naming conventions on.