Second large port from HoTT-categories

This brings in natural transformations, functor categories, initial and terminal categories, (in)discrete categories, and groupoid categories.

The next on the list are products of functors (which currently uses some moderately high-powered automation to prove that the product category satisfies the universal property of the product; so I might just drop that for now and only put it in the contrib folder later), the precategory of sets (which I still haven't quite managed to prove is a category), and the hom functor.  After that comes the definition of full and faithful, the Yoneda lemma, and subcategories.  I think then I'll try to formalize the structure identity principle, and eventually port the Rezk completion from http://arxiv.org/abs/1303.0584.  Finally, I'll work on porting the rest of my library to the contrib folder.