HoTT/HoTT — pull request #350 by JasonGross (2014-03-29 22:15:29+00:00)
Title: Structure identity principle

Formalize the structure identity principle. I hope to create a tactic which will take care of essentially all of the `IsCategory` instances via the structure identity principle and the `issig` tactics, together with a lemma that says that if `C` and `D` have equivalent types of objects, morphisms, and composition, then, `C` is a category iff `D` is.

I have also connected the extant category theory to theorems in the book. Some theorems were missing labels (https://github.com/HoTT/book/pull/653), so I stuck them in the nearest section in the mean time.

This include #347.