Universe is a concept which is present from the beginning of the creation of the Mizar Mathematical Library (MML) in several forms (Universe, Universe_closure, UNIVERSE) [25], then later as the_universe_of, [33], and recently with the definition GrothendieckUniverse [26], [11], [11]. These definitions are useful in many articles [28, 33, 8, 35], [19, 32, 31, 15, 6], but also [34, 12, 20, 22, 21], [27, 2, 3, 23, 16, 7, 4, 5].
In this paper, using the Mizar system [9] [10], we trivially show that Grothendieck’s definition of Universe as defined in [26], coincides with the original definition of Universe defined by Artin, Grothendieck, and Verdier (
Although a universe may be empty, we consider the properties of non-empty universes, completing the properties proved in [25].
We introduce the notion of “trivial” and “non-trivial” Universes, depending on whether or not they contain the set
The last section is devoted to the construction, in Tarski-Grothendieck, of a tower of universes indexed by the ordinal numbers (See 8. Examples, Grothendieck universe, ncatlab.org [24]).
Grothendieck’s universe is referenced in current works: “Assuming the existence of a sufficient supply of (Grothendieck) univers”, Jacob Lurie in “Higher Topos Theory” [17], “Annexe B – Some results on Grothendieck universes”, Olivia Caramello and Riccardo Zanfa in “Relative topos theory via stacks” [13], “Remark 1.1.5 (quoting Michael Shulman [30])”, Emily Riehl in “Category theory in Context” [29], and more specifically “Strict Universes for Grothendieck Topoi” [14].