Intrinsic Topology of the Universe

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Opening obstruction

In constructive univalent foundations, maps out of a universe can satisfy continuity principles that have no classical set-theoretic analogue.

Development contract

Freeze the TypeTopology assumptions, construct the intrinsic topology and prove the selected continuity/Rice-style consequence. State function extensionality, convergence and universe hypotheses at every export.