The intrinsic topology of Martin-Löf universes

详细信息    查看全文

• 作者：Martí ; n Hö ; tzel Escardó ; ^a ; ^{m.escardo@cs.bham.ac.uk" class="auth_mail" title="E-mail the corresponding author} ; Thomas Streicher^b
• 关键词：03B15 ; 03F50 ; 03C90 ; 03D65
• 刊名：Annals of Pure and Applied Logic
• 出版年：2016
• 出版时间：September 2016
• 年：2016
• 卷：167
• 期：9
• 页码：794-805
• 全文大小：281 K

文摘

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.