The strength of Martin-Löf type theory with a superuniverse. II
From MaRDI portal
Publication:5945010
DOI10.1007/s001530000051zbMath0990.03048OpenAlexW1970430231MaRDI QIDQ5945010
Publication date: 3 March 2002
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s001530000051
Nonclassical and second-order set theories (03E70) Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Recursive ordinals and ordinal notations (03F15)
Related Items
From type theory to setoids and back, Wellordering proofs for metapredicative Mahlo, Well-Ordering Principles in Proof Theory and Reverse Mathematics, Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice, Dependent products and 1-inaccessible universes, Unnamed Item, Proof Theory of Constructive Systems: Inductive Types and Univalence, Universes over Frege structures
