make clean now also cleans up the files generated by the index stuff.
thesis.idx needs to be ignored.
Fooled around a bit with the bibliography.
Added stuff from proposal to HoTT introduction and wrote some more on the homotopy part.