Set category

This implements the precategory of sets and the precategory of props, and proves that the latter is strict.  I've tried to prove that these are categories, but had some trouble.  If someone else wants to take a crack at this, the code is `theories/categories/SetCategory/Morphisms.v` in https://github.com/JasonGross/HoTT/tree/set-category-univalent.