Prove Theorem 7.2.2 from the book

I chose to use the first proof because I couldn't find 4.7.7 already in
the library.  I didn't use [dpath_forall] (which HoTTBook.v tells me is
2.9.6) because that requires [Funext], and this lemma doesn't need it.
Formalize the "notion of a structure"

Hopefully we'll soon be moving to polyproj, where I hope we won't have
to deal with this nonsense of defining simple record types for speed of
[destruct].