HoTT/HoTT — pull request #230 by JasonGross (2013-10-22 05:31:16+00:00)
Title: Set category

This is on top of #226.

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.