The intrinsic topology of Martin-Löf universes

A construction by Hofmann and Streicher gives an interpretation of a type-theoretic universe U in any Grothendieck topos, assuming a Grothendieck universe in set theory. Voevodsky asked what space U is interpreted as in Johnstone's topological topos. We show that its topological reflection is indiscrete. We also offer a model-independent, intrinsic or synthetic, description of the topology of the universe: It is a theorem of type theory that the universe is sequentially indiscrete, in the sense that any sequence of types converges to any desired type, up to equivalence. As a corollary we derive Rice's Theorem for the universe: it cannot have any non-trivial, decidable, extensional property, unless WLPO, the weak limited principle of omniscience, holds.