Non-trivial universes and sequences of universes

DOI10.2478/FORMA-2022-0005MaRDI QIDQ6489401

Roland Coghetto

Publication date: 22 April 2024

Published in: Formalized Mathematics (Search for Journal in Brave)

zbMATH Keywords

Grothendieck universeTarski-Grothendieck set theoryuniverse hierarchy

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Formalization of mathematics in connection with theorem provers (68V20)

Cites Work

• Unnamed Item
• Unnamed Item
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Grothendieck universes
• A tale of two set theories
• Seminar of algebraic geometry du Bois-Marie 1963--1964. Topos theory and étale cohomology of schemes (SGA 4). Vol. 1: Topos theory. Exp. I--IV
• Veblen Hierarchy
• Mizar: State-of-the-art and Beyond
• Higher Topos Theory (AM-170)

This page was built for publication: Non-trivial universes and sequences of universes