@ARTICLE{CLASSES5.ABS,
    TITLE = {{U}-Small and {U}-Locally Small Categories},
    ANNOTE = {This work has been supported by the 
    {\em Centre autonome de formation et de recherche en math{\'e}matiques et 
    sciences avec assistants de preuve}, 
    ASBL (non-profit organization). Enterprise number: 0777.779.751. Belgium.},
    DAY = {8},
    MONTH = {November},
    YEAR = {2024},
    AUTHOR = {Coghetto, Roland},
    ADDRESS1 = {cafr-MSA2P asbl\\Rue de la Brasserie 5\\7100 La Louvi\`ere, Belgium},
    SUMMARY = {Category theory is developed from the beginning of MML \cite{Mizar-State-2015}.
    Gradually it was expanded, with several different definitions for a category: 
    \verb+Category+ (\cite{CAT_1.ABS}) and
    \verb+category+ (in \cite{CAT_6.ABS} or with another definition in 
    \cite{ALTCAT_1.ABS}).
    In the following, we will only use, among these 3 definitions, the first, 
    as well as the notion $\mathcal{U}$ for Grothendieck's non-empty Universe.\par
    The first part of this work is devoted to the definitions of $\mathcal U$\verb+-set+ 
    and proper classes $\mathcal U$\verb+-class+.\par
    The second part is largely influenced by the number 0 \textit{Universe} of the first presentation 
    of SGA 4 \cite{artin1963theorie},
    we define the notion of a $\mathcal U$\verb+-small set+ (and of $\mathcal U$\verb+-small+ group 
    as well as of $\mathcal U$\verb+-small+ Category).
    This allows us to access the formalization of the definition of $\mathcal U$\verb-Category+.\par
    Finally, we introduce the notions of $\mathcal U$\verb+-small Category+ 
    and $\mathcal U$\verb+-locally small Category+ and
    some classic examples (adapted from "Example 1.1.4" by Emily Riehl in ``Category theory in Context"
    \cite{riehl2017category}).}, 
    MSC2010 = {03E70 18-00},
    KEYWORDS = {Tarski-Grothendieck set theory; Grothendieck universe; U-small category; 
       U-locally small category}}

