The intrinsic topology of Martin-Löf universes

DOI10.1016/j.apal.2016.04.010zbMath1402.03022OpenAlexW2186250550MaRDI QIDQ290640

Thomas Streicher, Martín Hötzel Escardó

Publication date: 3 June 2016

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2016.04.010

zbMATH Keywords

topologyuniverseMartin-Löf type theoryRice's theorem

Mathematics Subject Classification ID

Related Items (1)

Brouwer's fixed-point theorem in real-cohesive homotopy type theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Metric spaces in synthetic topology
• Realizability. An introduction to its categorical side
• A Convenient Category of Domains
• Infinite sets that Satisfy the Principle of Omniscience in any Variety of Constructive Mathematics
• On a Topological Topos
• A uniform approach to domain theory in realizability models
• Homotopy Type Theory: Univalent Foundations of Mathematics

This page was built for publication: The intrinsic topology of Martin-Löf universes