Added file explaining how to read HOTT in Coq

This is NOT finished.  Although the start is pretty smooth, now.

Works in CoqIDE 8.4
Works in ProofGeneral with HoTT-Coq/stable branch
Does NOT work with HoTT-Coq/stable's coqc from the command-line

Since it doesn't work with coqc, I can't generate the .glob file
necessary for running coqdoc yet.