The intrinsic topology of Martin-Löf universes
| Autor: | Martín Hötzel Escardó, Thomas Streicher |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Logic
Grothendieck universe media_common.quotation_subject 010102 general mathematics Rice's theorem Mathematics::General Topology 0102 computer and information sciences Intuitionistic type theory Topology 01 natural sciences Universe Topos theory Decidability Type theory 010201 computation theory & mathematics Mathematics::Category Theory 0101 mathematics Equivalence (formal languages) Mathematics media_common |
| Zdroj: | Annals of Pure and Applied Logic. 167:794-805 |
| ISSN: | 0168-0072 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect