U-Small and U-Locally Small Categories

This paper deals with the notions of U-small set, U-small category, and U-locally small category (U is non-empty Grothendieck universe). We reuse the first Mizar formalization of categories contained in CAT_* series of Mizar articles in order to show the expressive power of the Tarski-Grothendieck set theory (which is the base for the Mizar Mathematical Library) in this area. We encode parts of SGA 4 by Nicolas Bourbaki.