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.