@MISC{CLASSES4.MIZ,
  
 TITLE = {Non-trivial Universes and Sequences of Universes},
  
  AUTHOR = {Roland Coghetto\\cafr-MSA2P asbl},
   
  ADDRESS1 = {Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
   
  DAY = {30},
   
  MONTH = {April},
   
  YEAR = {2022},
  
  NOTE = {This work has been supported by the ``Centre autonome
   
  de formation et de recherche en mathématiques et sciences avec
   
  assistants de preuve” ASBL (non-profit organization).
   
  Enterprise number: 0777.779.751. Belgium},
  
  SUMMARY = {Universe is a concept which is present from the
   
  beginning of the creation of the MML in several forms
 (\verb+Universe+,
   
  \verb+Universe\_closure+, \verb+UNIVERS+),
  \cite{CLASSES2.ABS},
   
  then later as \verb+the_universe_of+, \cite{YELLOW_6.ABS}, 
  
  and recently with the definition
  \verb+GrothendieckUniverse+ 
  \cite{CLASSES3.ABS,brown2019tale}.
   
  These definitions are useful in many articles
   
  \cite{ALGSTR_4.ABS,YELLOW_6.ABS,YELLOW19.ABS,WAYBEL_5.ABS},
  
  \cite{WAYBEL_6.ABS,WAYBEL11.ABS,WAYBEL28.ABS,WAYBEL32.ABS,WAYBEL33.ABS},
    
  but also 
  \cite{CARD_LAR.ABS,ENS_1.ABS,GRCAT_1.ABS,MOD_2.ABS,MODCAT_1.ABS},
  
  \cite{NECKLA_2.ABS,ORDINAL4.ABS,ORDINAL6.ABS,RINGCAT1.ABS,ZF_FUND1.ABS,ZF_FUND2.ABS,ZFREFLE1.ABS,ZF_REFLE.ABS}
.
  
  In this paper, using the Mizar system \cite{Mizar-State-2015}, 

   we show that Grothendieck's definition of Universe as
  
  defined in \cite{CLASSES3.ABS}, coincides with the original 
   definition of Universe defined by Artin, Grothendieck, and 
  
  Verdier (\textit{Chapitre 0 Univers et Appendice ``Univers" (par N. Bourbaki) 
  
de l'Exposé I. "PREFAISCEAUX"})
  \cite{artin1963theorie},
  
  and how the different definitions of MML concerning
  universes are 
  related.
 We also show that the definition of Universe
 introduced by 
  Mac Lane (\cite{MacLane:1}) is 
  compatible with the MML's definition.\par
  
  Although a universe may be empty,
   we consider the properties  of 
  non-empty universes,
  completing the properties proved in   \cite{CLASSES2.ABS}.\par
  
  We introduce the notion of ``trivial" and  ``non-trivial" universes,
  
  depending on whether or not they contain the set \verb+NAT+
  
  (following the notion of Robert M.   Solovay
  
  {\footnote{https://cs.nyu.edu/pipermail/fom/2008-March/012783.html}).
  
  The following result links the universes FinSETS and SETS:
  
  \verb+GrothendieckUniverse omega = GrothendieckUniverse FinSETS = SETS+.\par
  
  Before turning to the last section, we establish some trivial propositions
  
  allowing the construction of sets outside the considered universe.\par
  
  The last section is
  devoted to the construction, in TG, of a universe 
  hierarchy sequence
    and a few properties.},
  
  MSC2010 = {03E70  68V20},
  
  KEYWORDS = {Tarski-Grothendieck set theory, Grothendieck 
   
    universe, universe hierarchy}}



@inproceedings{brown2019tale,
  
  title={A tale of two set theories},
  
  author={Brown, Chad E and P{\k{a}}k, Karol},
  
  booktitle={International Conference on Intelligent Computer Mathematics},
  
  pages={44--60},
  
  year={2019},
  
  organization={Springer}
}



@article{artin1963theorie,
  
  title={Th{\'e}orie des topos et cohomologie {\'e}tale des 
    sch{\'e}mas. Tome 1 Th{\'e}orie des topos (expos{\'e}s I {\`a} IV)},
  
  author={Artin, M and Grothendieck, A and Verdier, JL},
  
  journal={S{\'e}minaire de G{\'e}om{\'e}trie Alg{\'e}brique du Bois Marie},
  
  volume={1964},
  
  year={1963}
}

