{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T00:12:58Z","timestamp":1783901578745,"version":"3.55.0"},"reference-count":35,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,4,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>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].<\/jats:p>\n                  <jats:p>\n                    In this paper, using the Mizar system [9] [10], we trivially show that Grothendieck\u2019s definition of Universe as defined in [26], coincides with the original definition of Universe defined by Artin, Grothendieck, and Verdier (\n                    <jats:italic>Chapitre 0 Univers et Appendice \u201cUnivers\u201d (par N. Bourbaki) de l\u2019Expos\u00e9 I. \u201cPREFAISCE-AUX\u201d<\/jats:italic>\n                    ) [1], and how the different definitions of MML concerning universes are related. We also show that the definition of Universe introduced by Mac Lane ([18]) is compatible with the MML\u2019s definition.\n                  <\/jats:p>\n                  <jats:p>Although a universe may be empty, we consider the properties of non-empty universes, completing the properties proved in [25].<\/jats:p>\n                  <jats:p>\n                    We introduce the notion of \u201ctrivial\u201d and \u201cnon-trivial\u201d Universes, depending on whether or not they contain the set\n                    <jats:italic>\u03c9<\/jats:italic>\n                    (NAT), following the notion of Robert M. Solovay\n                    <jats:sup>2<\/jats:sup>\n                    . The following result links the universes\n                    <jats:bold>U<\/jats:bold>\n                    <jats:sub>0<\/jats:sub>\n                    (FinSETS) and\n                    <jats:bold>U<\/jats:bold>\n                    <jats:sub>1<\/jats:sub>\n                    (SETS):\n                    <jats:disp-formula>\n                      <jats:alternatives>\n                        <jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2022-0005_eq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"block\">\n                          <m:mrow>\n                            <m:mtext>Grothendieck<\/m:mtext>\n                            <m:mi>\u2009<\/m:mi>\n                            <m:mtext>Universe<\/m:mtext>\n                            <m:mi>\u2009<\/m:mi>\n                            <m:mi>\u03c9<\/m:mi>\n                            <m:mo>=<\/m:mo>\n                            <m:mtext>Grothendieck<\/m:mtext>\n                            <m:mi>\u2009<\/m:mi>\n                            <m:mtext>Universe<\/m:mtext>\n                            <m:mi>\u2009<\/m:mi>\n                            <m:msub>\n                              <m:mrow>\n                                <m:mstyle fontweight=\"bold\" fontstyle=\"normal\">\n                                  <m:mi>U<\/m:mi>\n                                <\/m:mstyle>\n                              <\/m:mrow>\n                              <m:mn>0<\/m:mn>\n                            <\/m:msub>\n                            <m:mo>=<\/m:mo>\n                            <m:msub>\n                              <m:mrow>\n                                <m:mstyle fontweight=\"bold\" fontstyle=\"normal\">\n                                  <m:mi>U<\/m:mi>\n                                <\/m:mstyle>\n                              <\/m:mrow>\n                              <m:mn>1<\/m:mn>\n                            <\/m:msub>\n                          <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>{\\rm{Grothendieck}}\\,{\\rm{Universe}}\\,\\omega = {\\rm{Grothendieck}}\\,{\\rm{Universe}}\\,{{\\bf{U}}_0} = {{\\bf{U}}_1}<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:disp-formula>\n                    Before turning to the last section, we establish some trivial propositions allowing the construction of sets outside the considered universe.\n                  <\/jats:p>\n                  <jats:p>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]).<\/jats:p>\n                  <jats:p>Grothendieck\u2019s universe is referenced in current works: \u201cAssuming the existence of a sufficient supply of (Grothendieck) univers\u201d, Jacob Lurie in \u201cHigher Topos Theory\u201d [17], \u201cAnnexe B \u2013 Some results on Grothendieck universes\u201d, Olivia Caramello and Riccardo Zanfa in \u201cRelative topos theory via stacks\u201d [13], \u201cRemark 1.1.5 (quoting Michael Shulman [30])\u201d, Emily Riehl in \u201cCategory theory in Context\u201d [29], and more specifically \u201cStrict Universes for Grothendieck Topoi\u201d [14].<\/jats:p>","DOI":"10.2478\/forma-2022-0005","type":"journal-article","created":{"date-parts":[[2022,12,21]],"date-time":"2022-12-21T05:26:11Z","timestamp":1671600371000},"page":"53-66","source":"Crossref","is-referenced-by-count":2,"title":["Non-Trivial Universes and Sequences of Universes"],"prefix":"10.2478","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4901-0766","authenticated-orcid":false,"given":"Roland","family":"Coghetto","sequence":"first","affiliation":[{"name":"cafr-MSA2P asbl, Rue de la Brasserie 5, 7100 La Louvi\u00e8re , Belgium"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2022,12,21]]},"reference":[{"key":"2026071212490921873_j_forma-2022-0005_ref_001","unstructured":"[1] M. Artin, A. Grothendieck, and J.L. Verdier. Th\u00e9orie des topos et cohomologie \u00e9tale des sch\u00e9mas. Tome 1: Th\u00e9orie des topos (expos\u00e9s i \u00e0 iv). S\u00e9minaire de G\u00e9om\u00e9trie Alg\u00e9brique du Bois Marie, Vol.1964."},{"key":"2026071212490921873_j_forma-2022-0005_ref_002","unstructured":"[2] Grzegorz Bancerek. Increasing and continuous ordinal sequences. Formalized Mathematics, 1(4):711\u2013714, 1990."},{"key":"2026071212490921873_j_forma-2022-0005_ref_003","doi-asserted-by":"crossref","unstructured":"[3] Grzegorz Bancerek. Veblen hierarchy. Formalized Mathematics, 19(2):83\u201392, 2011. doi:10.2478\/v10037-011-0014-5.","DOI":"10.2478\/v10037-011-0014-5"},{"key":"2026071212490921873_j_forma-2022-0005_ref_004","unstructured":"[4] Grzegorz Bancerek. Consequences of the reflection theorem. Formalized Mathematics, 1 (5):989\u2013993, 1990."},{"key":"2026071212490921873_j_forma-2022-0005_ref_005","unstructured":"[5] Grzegorz Bancerek. The reflection theorem. Formalized Mathematics, 1(5):973\u2013977, 1990."},{"key":"2026071212490921873_j_forma-2022-0005_ref_006","unstructured":"[6] Grzegorz Bancerek and Noboru Endou. Compactness of lim-inf topology. Formalized Mathematics, 9(4):739\u2013743, 2001."},{"key":"2026071212490921873_j_forma-2022-0005_ref_007","unstructured":"[7] Grzegorz Bancerek and Andrzej Kondracki. Mostowski\u2019s fundamental operations \u2013 Part II. Formalized Mathematics, 2(3):425\u2013427, 1991."},{"key":"2026071212490921873_j_forma-2022-0005_ref_008","unstructured":"[8] Grzegorz Bancerek, Noboru Endou, and Yuji Sakai. On the characterizations of compactness. Formalized Mathematics, 9(4):733\u2013738, 2001."},{"key":"2026071212490921873_j_forma-2022-0005_ref_009","doi-asserted-by":"crossref","unstructured":"[9] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-817.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026071212490921873_j_forma-2022-0005_ref_010","doi-asserted-by":"crossref","unstructured":"[10] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026071212490921873_j_forma-2022-0005_ref_011","unstructured":"[11] Chad E. Brown and Karol P\u0105k. A tale of two set theories. In Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics \u2013 12th International Conference, CICM 2019, CIIRC, Prague, Czech Republic, July 8-12, 2019, Proceedings, volume 11617 of Lecture Notes in Computer Science, pages 44\u201360. Springer, 2019. doi:10.1007\/978-3-030-23250-44."},{"key":"2026071212490921873_j_forma-2022-0005_ref_012","unstructured":"[12] Czes\u0142aw Byli\u0144ski. Category Ens. Formalized Mathematics, 2(4):527\u2013533, 1991."},{"key":"2026071212490921873_j_forma-2022-0005_ref_013","unstructured":"[13] Olivia Caramello and Riccardo Zanfa. Relative topos theory via stacks. arXiv preprint arXiv:2107.04417, 2021."},{"key":"2026071212490921873_j_forma-2022-0005_ref_014","unstructured":"[14] Daniel Gratzer, Michael Shulman, and Jonathan Sterling. Strict universes for Grothendieck topoi. arXiv preprint arXiv:2202.12012, 2022."},{"key":"2026071212490921873_j_forma-2022-0005_ref_015","unstructured":"[15] Ewa Gr\u0105dzka. On the order-consistent topology of complete and uncomplete lattices. Formalized Mathematics, 9(2):377\u2013382, 2001."},{"key":"2026071212490921873_j_forma-2022-0005_ref_016","unstructured":"[16] Andrzej Kondracki. Mostowski\u2019s fundamental operations \u2013 Part I. Formalized Mathematics, 2(3):371\u2013375, 1991."},{"key":"2026071212490921873_j_forma-2022-0005_ref_017","doi-asserted-by":"crossref","unstructured":"[17] Jacob Lurie. Higher Topos Theory. Princeton University Press, 2009.10.1515\/9781400830558","DOI":"10.1515\/9781400830558"},{"key":"2026071212490921873_j_forma-2022-0005_ref_018","unstructured":"[18] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, Heidelberg, Berlin, 1971."},{"key":"2026071212490921873_j_forma-2022-0005_ref_019","unstructured":"[19] Beata Madras. Irreducible and prime elements. Formalized Mathematics, 6(2):233\u2013239, 1997."},{"key":"2026071212490921873_j_forma-2022-0005_ref_020","unstructured":"[20] Micha\u0142 Muzalewski. Categories of groups. Formalized Mathematics, 2(4):563\u2013571, 1991."},{"key":"2026071212490921873_j_forma-2022-0005_ref_021","unstructured":"[21] Micha\u0142 Muzalewski. Category of left modules. Formalized Mathematics, 2(5):649\u2013652, 1991."},{"key":"2026071212490921873_j_forma-2022-0005_ref_022","unstructured":"[22] Micha\u0142 Muzalewski. Rings and modules \u2013 part II. Formalized Mathematics, 2(4):579\u2013585, 1991."},{"key":"2026071212490921873_j_forma-2022-0005_ref_023","unstructured":"[23] Micha\u0142 Muzalewski. Category of rings. Formalized Mathematics, 2(5):643\u2013648, 1991."},{"key":"2026071212490921873_j_forma-2022-0005_ref_024","unstructured":"[24] nLab Authors. Grothendieck universe, 2022."},{"key":"2026071212490921873_j_forma-2022-0005_ref_025","unstructured":"[25] Bogdan Nowak and Grzegorz Bancerek. Universal classes. Formalized Mathematics, 1(3): 595\u2013600, 1990."},{"key":"2026071212490921873_j_forma-2022-0005_ref_026","doi-asserted-by":"crossref","unstructured":"[26] Karol P\u0105k. Grothendieck universes. Formalized Mathematics, 28(2):211\u2013215, 2020. doi:10.2478\/forma-2020-0018.","DOI":"10.2478\/forma-2020-0018"},{"key":"2026071212490921873_j_forma-2022-0005_ref_027","unstructured":"[27] Krzysztof Retel. The class of series-parallel graphs. Part II. Formalized Mathematics, 11 (3):289\u2013291, 2003."},{"key":"2026071212490921873_j_forma-2022-0005_ref_028","doi-asserted-by":"crossref","unstructured":"[28] Marco Riccardi. Free magmas. Formalized Mathematics, 18(1):17\u201326, 2010. doi:10.2478\/v10037-010-0003-0.","DOI":"10.2478\/v10037-010-0003-0"},{"key":"2026071212490921873_j_forma-2022-0005_ref_029","unstructured":"[29] Emily Riehl. Category theory in context. Courier Dover Publications, 2017."},{"key":"2026071212490921873_j_forma-2022-0005_ref_030","unstructured":"[30] Michael A. Shulman. Set theory for category theory. arXiv preprint arXiv:0810.1279, 2008."},{"key":"2026071212490921873_j_forma-2022-0005_ref_031","unstructured":"[31] Bart\u0142omiej Skorulski. Lim-inf convergence. Formalized Mathematics, 9(2):237\u2013240, 2001."},{"key":"2026071212490921873_j_forma-2022-0005_ref_032","unstructured":"[32] Andrzej Trybulec. Scott topology. Formalized Mathematics, 6(2):311\u2013319, 1997."},{"key":"2026071212490921873_j_forma-2022-0005_ref_033","unstructured":"[33] Andrzej Trybulec. Moore-Smith convergence. Formalized Mathematics, 6(2):213\u2013225, 1997."},{"key":"2026071212490921873_j_forma-2022-0005_ref_034","unstructured":"[34] Josef Urban. Mahlo and inaccessible cardinals. Formalized Mathematics, 9(3):485\u2013489, 2001."},{"key":"2026071212490921873_j_forma-2022-0005_ref_035","unstructured":"[35] Mariusz \u0142ynel. The equational characterization of continuous lattices. Formalized Mathematics, 6(2):199\u2013205, 1997."}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2022-0005","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,13]],"date-time":"2026-07-13T00:03:44Z","timestamp":1783901024000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2022-0005"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,1]]},"references-count":35,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2022,12,21]]},"published-print":{"date-parts":[[2022,4,1]]}},"alternative-id":["10.2478\/forma-2022-0005"],"URL":"https:\/\/doi.org\/10.2478\/forma-2022-0005","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,1]]}}}