Non-trivial universes and sequences of universes

DOI10.2478/FORMA-2022-0005MaRDI QIDQ6489401zbMATH OpenFDO

Authors Roland Coghetto

Publication date 22 April 2024

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

Full work available at URL https://doi.org/10.2478/FORMA-2022-0005

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)

Recommendations

• Grothendieck universes
• scientific article; zbMATH DE number 3279146
• scientific article; zbMATH DE number 1302063
• scientific article; zbMATH DE number 2247252

Cites work

• A tale of two set theories
• Category theory in context
• Grothendieck universes
• Higher Topos Theory (AM-170)
• scientific article; zbMATH DE number 3367095 (Why is no real title available?)
• Mizar: state-of-the-art and beyond
• 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
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Veblen hierarchy

Cited in

(2)

• Grothendieck universes
• U-small and U-locally small categories

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6489401)