merge of old HoTT.tex with new diSimplexTheory paper