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.

This includes #347.