Non-trivial universes and sequences of universes

DOI10.2478/FORMA-2022-0005MaRDI QIDQ6489401FDOQ6489401

Authors: Roland Coghetto 

Publication date: 22 April 2024

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

Recommendations

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

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

• 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
• Higher Topos Theory (AM-170)
• Title not available (Why is that?)
• Veblen hierarchy
• Category theory in context
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Grothendieck universes
• A tale of two set theories

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)