Pruned various usages of "homotopy type" to avoid confusing the reader, feel free
to re-qualify.

Changed a sentence just after the Unvialence axiom from

	From the homotopical point of view, this says that the universe $\UU$
	is something like a classifying space for (small) homotopy types, which
	is a practical and natural assumption.

to

	From the homotopical point of view, this implies that the universe
	$\UU$, viewed as a classifying space for (small) spaces, connects
	spaces of the same homotopy type, in accord with intuition.