formal.tex: explaining definitions and rewording hott axioms section