Reference. Universes for Category Theory [low-universes-category-theory-2014]

November 28, 2014
Low, Zhen Lin
https://arxiv.org/pdf/1304.5227.pdf

Backlinks

Definition. (Essentially/Locally) small categories [002o]

November 27, 2025

Definition. Small category

November 27, 2025

A category \(\mathcal {C}\) is called small (or \(U\)-small) if both the collection of objects \(\mathrm {Ob}(\mathcal {C})\) and the collection of morphisms \(\mathrm {Mor}(\mathcal {C})\) are sets (i.e. elements of the universe \(U\)). In lean where we correspond universes to types this just means that we instatiate the universe levels of morphisms and objects to the same thing, we can see this clearly in the definition of a \(\texttt {SmallCategory}\) in mathlib.


    abbrev SmallCategory (C : Type u) : Type (u + 1) := Category.{u} C

Definition. Locally small

November 27, 2025

A locally small category \(\mathcal {C}\) is a category satisfying the following conditions:

The collection of objects \(\mathrm {Ob}(\mathcal {C})\) and morphisms \(\mathrm {Mor}(\mathcal {C})\) are classes. (1)
For every pair of objects \(X, Y \in \mathrm {Ob}(\mathcal {C})\) the hom-set \(\mathcal {C}(X, Y)\) is a set (or small set) instead of a proper class.

The lean definition

November 27, 2025

This one is a little bit more interesting, first let's look at the definition in mathlib:


      class Small (α : Type v) : Prop where
        /-- If a type is `Small.{w}`, 
          then there exists an equivalence with some `S : Type w` -/
        equiv_small : ∃ S : Type w, Nonempty (α ≃ S)

      ...
      class LocallySmall (C : Type u) [Category.{v} C] : Prop where
        /-- A locally small category has small hom-types. -/
        hom_small : ∀ X Y : C, Small.{w} (X ⟶ Y) := by infer_instance

So we can see that in lean a locally small category is defined as a normal category with the added property that for every pair of objects \(X, Y \in \mathrm {Ob}\) the hom-type \(X ⟶ Y\) is \(\texttt {Small}\), which as we can see from the definition of \(\texttt {Small}\) means that there exists some type \(\texttt {S : Type w}\) such that there is an equivalence \(α ≃ S\). We can informally correspond to the lean definition as follows:

Our objects \(\texttt {C : Type u}\) live in some universe level \(u\) which we assoicate with being a class i.e. possibly large collection.
The morphisms between any two objects \(\texttt {X, Y : C}\) live in some other universe level \(w\) where the equivalence to some type \(\texttt {S : Type w}\) expresses the notion that the hom-sets are small sets.

Honestly I think quite reasonably its fair to ask: wait what how does that represent smallness ? What is \(\texttt {w}\) even supposed to be? So I think an example is warranted.

Example of a locally small category

November 27, 2025

This is arguably a bit contrived but let's consider objects as being containers for types in some universe level \(0\) i.e. sets. So we can define our objects and morphisms as follows:


      structure TWrapper : Type 1 where
        carrier : Type 0

      /-- Morphisms are functions - each Hom(A,B) is a set -/
      def TWHom (A B : TWrapper) : Type 0 := A.carrier → B.carrier

Importantly we can note here that the type of objects \(\texttt {TWrapper : Type 1}\) lives in universe level \(1\) which we can think of as a class of sets. However the morphisms between any two objects \(\texttt {TWHom (A B : TWrapper) : Type 0}\) live in universe level \(0\) which we can think of as small sets. Using this we can define a category instance:


      instance TWrapper.category : Category TWrapper where
        -- The data
        Hom     := TWHom
        id      := fun _ => id
        comp    := 
          fun {X Y Z} (f : TWHom X Y) (g : TWHom Y Z) => fun x => g (f x)

        -- The laws
        id_comp := fun _ => rfl
        comp_id := fun _ => rfl
        assoc := fun _ _ _ => rfl

Now we want to define the locally small instance:


      instance TWrapper.locallySmall : LocallySmall.{0} TWrapper where
        hom_small := fun X Y => ⟨⟨TWHom X Y, ⟨Equiv.refl _⟩⟩⟩

This now answers a few questions that arose earlier:

We instantiated the universe level of our hom-sets \(\texttt {w}\) to \(0\) which corresponds to small sets.
The equivalence \(\texttt {α ≃ S}\) in this case is just the identity equivalence \(\texttt {Equiv.refl}\) since our hom-sets are already small sets. On other words here:
```
        Small.{w} (X ⟶ Y)
      
```
We have that \(\texttt {X ⟶ Y}\) represents our set which exists in universe level \(0\), since we are instantiating \(\texttt {w}\) to \(0\) the \(\texttt {Small}\) definition is satisfied by the identity equivalence.

So we can see that in the context of lean a locally small category is just a category where the objects live in some universe level (class) and the hom-sets live in some smaller universe level (set) and we must provide an equivalence showing that the hom-sets are indeed small sets.

Definition. Essentially small

November 27, 2025

A category \(\mathcal {C}\) is called essentially small if there exists a small category \(\mathcal {D}\) and a functor:

\[ F : \mathcal {D} \to \mathcal {C} \]

That is fully faithful and essentially surjective on objects, i.e. it represents an equivalence. In other words we call a category essentially small if its isomorphism classes of objects form a set.

To elaborate a bit more, we say that a functor \(F : C \to D\) is an equivalence if there exists:

A functor \(G : D \to C\)
The natural isomorphisms: \[ \eta : \text {Id}_C \xrightarrow {\cong } G \circ F \quad \epsilon : F \circ G \xrightarrow {\cong } \text {Id}_D \] in other words the natural transformations \(\eta \) and \(\epsilon \) are isomorphisms. Equivalently using diagrammatic notation we can express this as: \[ \eta : 1_C \xrightarrow {\cong } F ; G \quad \epsilon : G ; F \xrightarrow {\cong } 1_D \] in plain english we can see this as saying that the round trip we take by applying \(F\) then \(G\) (or vice versa) is naturally isomorphic to doing nothing at all (the identify functor).

In diagrammatic form we can represent this as follows:

The main takeaway here being that an essentially small category is one which is equivalent to a small category. Hence the problem of demonstrating a category is essentially small reduces to demonstrating isomorphisms between the unit and counit natural transformations.

The lean definition

November 27, 2025

We can again examine the definition in mathlib:


      /-- A category is `EssentiallySmall.{w}` if there exists
      an equivalence to some `S : Type w` with `[SmallCategory S]`. -/
      @[pp_with_univ]
      class EssentiallySmall (C : Type u) [Category.{v} C] : Prop where
        /-- An ES category is equivalent to some small category. -/
        equiv_smallCategory : ∃ (S : Type w) (_ : SmallCategory S), Nonempty (C ≌ S)

We can see quite nicely here how the lean definition corresponds to the informal one. We have our category \(\texttt {C : Type u}\) living in some universe level \(u\) (class) and we require the existence of some small category \(\texttt {S : Type w}\) living in some smaller universe level \(w\) (set) such that there exists an equivalence \(\texttt {C ≌ S}\).

Example of an essentially small category

November 27, 2025

As an example we will take the categories \(\texttt {FinSet}\) and \(\texttt {FinOrd}\). Starting with the former, the category of finite sets \(\texttt {FinSet}\) is defined as follows:


      /-- Finite sets as a category - objects are Fin n for various n -/
      structure FinSetObj : Type 1 where
        n : ℕ
        carrier : Type 0
        equiv   : carrier ≃ Fin n  -- witness that carrier has exactly n elements

      /-- Morphisms are functions between the carriers -/
      def FSHom (A B : FinSetObj) : Type 0 := A.carrier → B.carrier

      /-- First, we need a Category instance -/
      instance FinSetObj.category : Category FinSetObj where
        Hom     := FSHom
        id      := fun _ => id
        comp    :=
          fun {X Y Z} (f : FSHom X Y) (g : FSHom Y Z) => fun x => g (f x)

        id_comp := fun _ => rfl
        comp_id := fun _ => rfl
        assoc   := fun _ _ _ => rfl

It's defined as the category who's objects are finite sets and who's morphisms are functions between said sets. Here we are defining a custom variant of a finite set object \(\texttt {FinSetObj}\) which contains:

A natural number \(\texttt {n : ℕ}\) representing the cardinality of the set.
A carrier type \(\texttt {carrier : Type 0}\) representing the actual elements of the set.
An equivalence \(\texttt {equiv : carrier ≃ Fin n}\) which acts as a witness that the carrier has exactly \(\texttt {n}\) elements.

We then define our morphisms as functions between the carrier types of two finite set objects. Finally we provide a category instance in the standard way.

Next we want to define the category of all finite ordinal numbers \(\texttt {FinOrd}\). This is defined as follows:


      /-- The skeleton: the discrete category on ℕ -/
      abbrev FinSetSkeleton := ℕ

      /-- The skeleton category: 
        objects are ℕ, morphisms are functions between Fin types -/
      structure FinSkel : Type 0 where
        n : ℕ

      instance : SmallCategory FinSkel where
        Hom   := fun A B => Fin A.n → Fin B.n
        id    := fun _ => id
        comp  := fun f g => g ∘ f

In our case we can define the finite ordinals as the skeleton of the finite sets category. So our objects are just natural numbers \(\texttt {n : ℕ}\) representing the finite ordinals and our morphisms are functions between the corresponding finite sets \(\texttt {Fin n}\). Again we provide a small category instance in the standard way.

Now central to the definition of an essentially small category is the existence of an equivalence, in other words we need to functors with a natural transformation witnessing the equivalence. We'll start by defining the functor from the finite ordinals to the finite sets:


      /-- Canonical embedding of FinSkel into FinSetObj -/
      def skelToFinSetObj : FinSkel ⥤ FinSetObj where
        obj       := fun A => ⟨A.n, Fin A.n, Equiv.refl _⟩
        map       := fun f => f
        map_id    := fun _ => rfl
        map_comp  := fun _ _ => rfl

We can note here that:

The object mapping takes a finite ordinal \(\texttt {A : FinSkel}\) and maps it to the corresponding finite set object with carrier \(\texttt {Fin A.n}\). The equivalence is just the identity equivalence since \(\texttt {Fin A.n}\) obviously has exactly \(\texttt {A.n}\) elements.
The morphism mapping is just the identity since morphisms in both categories are functions between finite sets.
The functor laws are satisfied by reflexivity.

The other way around is a little bit more involved, we can construct the functor as follows:


      def finSetObjToSkel : FinSetObj ⥤ FinSkel where
        obj := fun A => ⟨A.n⟩
        map := fun {A B} f => B.equiv ∘ f ∘ A.equiv.symm
        map_id := fun A => by
          funext x
          show A.equiv ((id : A.carrier → A.carrier) (A.equiv.symm x)) 
            = (id : Fin A.n → Fin A.n) x

          simp only [id_eq, Equiv.apply_symm_apply]
        map_comp := fun {A B C} f g => by
          funext x
          show C.equiv (g (f (A.equiv.symm x))) 
            = (C.equiv ∘ g ∘ B.equiv.symm) ((B.equiv ∘ f ∘ A.equiv.symm) x)

          simp only [Function.comp_apply, Equiv.symm_apply_apply]

Again to break this down by components:

In the object mapping we are taking in a finite set object \(\texttt {A : FinSetObj}\) and mapping it to the corresponding finite ordinal represented by the natural number \(\texttt {A.n}\).
Our morphism mapping is a bit more complex, since we are going from the category of finite sets our source and target objects \(\texttt {A}\) and \(\texttt {B}\) represent the finite set objects. For all pairs of objects the map function demands:
```
          ∀ {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y))
        
```
we are provided with the set of morphisms \(\texttt {f : A.carrier → B.carrier}\) and we need to produce a function between the corresponding finite sets \(\texttt {Fin A.n → Fin B.n}\). Here we utilize an important property that comes with equivalences: they can be used to transport functions between types. To explain what this means let's consider the isolated example:


          variable (A B : FinSetObj) (f : FinSetObj.category.Hom A B)

          #check B.equiv ∘ f      -- ⇑B.equiv ∘ f : A.carrier → Fin B.n
          #check f ∘ A.equiv.symm -- f ∘ ⇑A.equiv.symm : Fin A.n → B.carrier


          @[simp, norm_cast]
          lemma _root_.EquivLike.coe_coe {F} [EquivLike F α β] (e : F) :
              ((e : α ≃ β) : α → β) = e := rfl


          ⇑B.equiv      B.carrier → Fin B.n
          ⇑A.equiv.symm Fin A.n   → A.carrier


          A.carrier → B.carrier → Fin B.n -- so A.carrier → Fin B.n
          Fin A.n → A.carrier → B.carrier -- so Fin A.n → B.carrier

Next we want to show that the functor preserves identities. In our case this means the following:
```
          map_id : ∀ (A : FinSetObj), 
            ⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm = 𝟙 { n := A.n }
        
```
As our probelm is of the shape \[ (\forall x, f x = g x) \] We can apply the \(\texttt {funext}\) tactic which reduces the goal to showing that the two sides are equal when applied to an arbitrary input \(\texttt {x}\). Our goal then becomes:
```
          (⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x = (𝟙 { n := A.n }) x
        
```
It might be helpful at this point to take a look at the underlying types:
```
          ... : Fin { n := A.n }.n → Fin { n := A.n }.n 
          = 
          ... :     { n := A.n }   ⟶     { n := A.n }
        
```
The purpose of the \(\texttt {show}\) tactic here is to explicitly specify the goal we want to prove, i.e. create a definitionally equal variant of the goal to replace the current one with, if we look at the goals before and after the show tactic we have:
```
          -- before
          ⊢ (⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x = 𝟙 { n := A.n } x

          -- after 
          ⊢ A.equiv (id (A.equiv.symm x)) = id x
        
```
looking at the types of the goal after the \(\texttt {show}\) tactic we have:
```
          ... : Fin A.n
          = 
          ... : Fin A.n
        
```
our final two simplifications then do
```
          A.equiv (id (A.equiv.symm x)) = A.equiv (A.equiv.symm x)
          
          -- id_eq : ... (a : α), id a = a
          A.equiv (A.equiv.symm x) = x

          -- apply_symm_apply : ... (e : α ≃ β) (x : β), e (e.symm x) = x
          x = x
        
```
For the sake of completeness I want to go into the \(\texttt {show}\) tactic a bit more. Startign with the right hand side, after the funext we have:
```
          𝟙 { n := A.n } x 
        
```
The braces here are just syntactic sugar for defining a FinSkel structure inline, so unfolding it we can equivalently display this as:
```
          variable (A : FinSetObj) (x : Fin (FinSkel.mk A.n).n)
          #check FinSkel.cat.id (FinSkel.mk A.n) x
        
```
but what we can notice if we look at the definition of our category is that the arrows between objects are actually arrows between their \(\texttt {n}\) fields (with the Fin proof) i.e.
```
          fun A B => Fin A.n → Fin B.n
        
```
so in reality our identity morphism is actually:
```
          𝟙 { n := A.n } : Fin A.n → Fin A.n
        
```
hence applying it to \(\texttt {x}\) gives us:
```
          (𝟙 { n := A.n }) x = id x
        
```
The left hand side follows a similar logic, in that we can again replace the identity morphism on the object with the identity function on the carrier type directly so we have:
```
          (⇑A.equiv ∘ 𝟙 A ∘ ⇑A.equiv.symm) x 
            -> (⇑A.equiv ∘ id ∘ ⇑A.equiv.symm) x
        
```
and then if we avoid the syntactic sugar of function composition we have:
```
          ⇑A.equiv (id (⇑A.equiv.symm x)) 
        
```
we can equivalently just automate this step by just prepending \(\texttt {Function.comp}\) into our simplification steps.
For the case of showing that our functor preserves composition of morphisms we have a similar situation as to the identity case, here just to keep things not dragging on too long i'll just say that again we are more or less following the same logic as before. We are using show to reduce or goal into a form that is easier to reason about, and then we are just simplifying using the properties of equivalences and function composition.

Moving on we now have two create our natural transformations, here things should now be rather straightforward. In lean we have:


      def unitNatTrans 
          : 𝟭 FinSetObj ⟶ finSetObjToSkel ⋙ skelToFinSetObj where
        app := fun A => (A.equiv : A.carrier → Fin A.n)
        naturality := fun A B f => by
          funext x
          show B.equiv (f x) 
            = (B.equiv ∘ f ∘ A.equiv.symm) (A.equiv x)
          simp only [Function.comp_apply, Equiv.symm_apply_apply]

      def unitInvNatTrans 
          : finSetObjToSkel ⋙ skelToFinSetObj ⟶ 𝟭 FinSetObj where
        app := fun A => (A.equiv.symm : Fin A.n → A.carrier)
        naturality := fun A B f => by
          funext x
          show B.equiv.symm ((B.equiv ∘ f ∘ A.equiv.symm) x) 
            = f (A.equiv.symm x)
          simp only [Function.comp_apply, Equiv.symm_apply_apply]

      /-- The unit isomorphism -/
      def unitIsoFinSetObj : 𝟭 FinSetObj ≅ finSetObjToSkel ⋙ skelToFinSetObj where
        hom := unitNatTrans
        inv := unitInvNatTrans
        hom_inv_id := by
          ext A
          funext x
          show A.equiv.symm (A.equiv x) = x
          simp only [Equiv.symm_apply_apply]
        inv_hom_id := by
          ext A
          funext x
          show A.equiv (A.equiv.symm x) = x
          simp only [Equiv.apply_symm_apply]

in lean composition of functors is denoted by the operator \(\texttt {⋙}\) so we can see that our unit natural transformation has the correct type. The components of the natural transformation are just given by the equivalences we have in our finite set objects, and the naturality conditions again follow from unfolding the definitions and simplifying.


      /-- Naturality lemma for counit transformations -/
      lemma counit_naturality {A B : FinSkel} (f : A ⟶ B) :
        (𝟭 FinSkel).map f ≫ id = id ≫ (skelToFinSetObj ⋙ finSetObjToSkel).map f := by
        simp only [Functor.id_obj, Functor.comp_obj, skelToFinSetObj, finSetObjToSkel]
        simp only [Functor.id_map, Functor.comp_map]
        rfl

      /-- The counit natural transformation: skelToFinSetObj ⋙ finSetObjToSkel → id -/
      def counitNatTrans : skelToFinSetObj ⋙ finSetObjToSkel ⟶ 𝟭 FinSkel where
        app := λ _ => id
        naturality := fun _ _ f => counit_naturality f |>.symm

      /-- The inverse of counit -/
      def counitInvNatTrans : 𝟭 FinSkel ⟶ skelToFinSetObj ⋙ finSetObjToSkel where
        app := λ _ => id
        naturality := fun _ _ f => counit_naturality f

      /-- The counit isomorphism -/
      def counitIsoFinSkel : skelToFinSetObj ⋙ finSetObjToSkel ≅ 𝟭 FinSkel where
        hom := counitNatTrans
        inv := counitInvNatTrans
        hom_inv_id := by ext A; rfl
        inv_hom_id := by ext A; rfl

Finally we can define the equivalence and then construct the essentially small instance:


      /-- The equivalence between FinSetObj and FinSkel -/
      def finSetObjEquiv : FinSetObj ≌ FinSkel where
        functor := finSetObjToSkel
        inverse := skelToFinSetObj
        unitIso := unitIsoFinSetObj
        counitIso := counitIsoFinSkel
        functor_unitIso_comp := fun A => by
          funext x
          show (id : Fin A.n → Fin A.n) (A.equiv (A.equiv.symm x)) = x
          simp only [id_eq, Equiv.apply_symm_apply]

      /-- Now we show FinSetObj is essentially small.
          We construct an explicit equivalence with the small category FinSkel. -/
      instance FinSetObj.essentiallySmall : EssentiallySmall.{0} FinSetObj :=
        EssentiallySmall.mk' finSetObjEquiv

Definition. Grothendieck universe [002q]

November 27, 2025

Motivation

November 27, 2025

In set theory (along with other theories which consider collections of stuff) there is an issue which you try to talk about the collection of collections, as it gives rise to certain paradoxes by the recursive nature of it. One way out is to consider a hierarchy of notions of collections, where a "collection of collections" is not in fact considered a "collection" itself but rather some notion of a higher increment of collection.

This is the idea behind universes, where the universe is a collection of all set's which intuitively can be thought of as a "set of all sets" but is not itself a set but one increment above it in the hierarchy.

Definition

November 27, 2025

A Grothendieck universe is a set (in ZFC) \(\mathcal U\) with the following properties (1):

(transitivity) If \(x \in \mathcal U\) and \(y \in x\), then \(y \in \mathcal U\).
(power set) If \(x \in \mathcal U\), then \(\mathcal P(x) \in \mathcal U\) where \(\mathcal P(x)\) is the powerset (set of all subsets) of \(x\).
(unions) If \(I \in \mathcal U\) and \(x_i \in \mathcal U\) for each \(i \in I\), then the union \[ \bigcup _{i \in I} x_i \in \mathcal U \]
(natural numbers) The set of natural numbers \(\mathbb {N} \in \mathcal U\).

Additional properties of \(\mathcal U\) can be enumerated as follows:

If \(x, y \in \mathcal U\) then \(\{x, y\} \in \mathcal U\).
If \(x \in \mathcal U\) and \(y \subset x\), then \(y \in \mathcal U\).
If \(I \in \mathcal U\) and \(x_i \in \mathcal U\) for each \(i \in I\), we have the cartesian product: \[ \prod _{i \in I} x_i \in \mathcal U \]
If \(I \in \mathcal U\) and \(x_i \in \mathcal U\) for each \(i \in I\), we have the disjoint union: \[\coprod _{i \in I} x_i \in \mathcal U \]
If \(x, y \in \mathcal U\), then the function set from \(x\) to \(y\) is also in \(\mathcal U\): \[ y^x = \{ f : x \to y \} \in \mathcal U \]

An aside on classes and sets

November 27, 2025

In a very general sense a class is any collection of sets defined by a property that all its members share. So we can express it it as a predicate on some universe \(\mathcal U\):

\[ A : \mathcal U \to \texttt {Prop} \]

As an example in the case of an unsorted set theory (such as ZFC) in which all objects are sets, we define a class \(C\) as a proposition or truth value in the context of some free variable \(A\), the notation used in (5) is:

\[ \Gamma , A \mid \phi \vdash C : \texttt {Prop} \]

This expresses that in the context of assumptions \(\Gamma \) extended with the variable \(A\) the proposition \(\phi \) defines a class \(C\). A more classical, albiet probably less formal, way to read this might be:

\[ C = \{ x \in \mathcal U \mid \phi (x)\} \]

Furthermore we say that a class \(X\) is a set if and only if there exists a class \(Y \in \mathcal U\) such that \(X \in Y\). A proper class is a class which is not a set (6).

Axiom of Universes

November 27, 2025

The common theme amongst these properties is that the aim to express closure of the set \(\mathcal U\) under various standard set-theoretic operations. This allows us to treat \(\mathcal U\) as a universe of sets in which we can carry out normal set-theoretic constructions without leaving the universe.

The Axiom of Universes is the general convention which is adopted in category theory and other fields which states that for every set \(x\) there exists a Grothendieck universe \(\mathcal U\) such that \(x \in \mathcal U\).

An element of \(\mathcal U\) is by convention called a \(\mathcal U\)-small set or simply a small set when the universe is clear from context or apparently also just a set (1).

A subset of \(\mathcal U\) is called \(\mathcal U\)-moderate or simply moderate when the universe is clear from context.

The general line of reasoning, at least in ZFC is that for every set \(x\) we assume there exists a Grothendieck universe \(\mathcal U\) such that \(x \in \mathcal U\). Accordinly for every universe \(\mathcal U\) there exists a larger universe \(\mathcal U'\) such that \(\mathcal U \in \mathcal U'\), and therefore also \(U \subseteq U'\). Thus under this assumption with have the guarantee of a hierarchy of universes (4):

\[ \mathcal U_0 \in \mathcal U_1 \in \mathcal U_2 \in \cdots \]

Which are also cumulative in the sense that

\[ \mathcal U_0 \subseteq \mathcal U_1 \subseteq \mathcal U_2 \subseteq \cdots \]

Remarks

November 27, 2025

An additional point made in (2) is that \(\mathcal U\) denotes a pure set, that is, all elements of \(\mathcal U\) are sets and there are no urelements (elements which are not sets). Formally we say that a set \(x\) is pure if for every finite sequence or chain (3):
\[ x_0 = x \in x_1 \in x_2 \in \cdots \in x_n \]
each \(x_i\) is a set. Another way this is intuitively thought of is that every object reachable from \(x\) by finitely many membership steps is also a set.

Since we are typically working in the context of ZFC set theory which only allows for sets as elements, all sets are pure by default hence the distinction is sometimes omitted. Theories such as ZFA (Zermelo-Fraenkel set theory with atoms) allow for urelements which do not qualify as sets but can be members of sets.
The countable set property is sometimes (7) also replaces with
\[ \emptyset \in \mathcal U \quad \text { or } \quad \omega \in \mathcal U \]
Where \(\omega \) is the set of all finite (von Neumann) ordinals.
Subset's of \(\mathcal U\) seem to have a somewhat confusing naming convention. So nlab says they are called moderate though this is sometimes also overloaded with the ambiguous term large. They mention that under the assumption that set is equivalent to small set then moderate clearly aligns with proper classes (as those are definitionally distinct from sets). I assume the convention taken in at least (1) is that they use they essentially use the term class to mean proper class and by implication moderate set relative to some universe.

My assumption is that people use class and proper class interchangeably mainly because a proper class actually refers to an object distinct from a set, whereas a class can make it ambiguous whether you mean a set (which is a class) or a proper class (which is not a set).