Grothendieck universes

DOI10.2478/FORMA-2020-0018OpenAlexW4253706475MaRDI QIDQ2113837FDOQ2113837

Karol Pąk

Publication date: 14 March 2022

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

Full work available at URL: https://doi.org/10.2478/forma-2020-0018

zbMATH Keywords

Grothendieck universeTarski-Grothendieck set theoryTarski's axiom A

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
• Title not available (Why is that?)
• The role of the Mizar mathematical library for interactive proof development in Mizar
• A tale of two set theories

Cited In (2)

• Combining higher-order logic with set theory formalizations
• Non-trivial universes and sequences of universes

Uses Software

• Mizar

This page was built for publication: Grothendieck universes

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