Class
A class is a Collection of different things with Propositional equality which may not be a set, though the exact meaning depends on the foundation being used. Thus it is a generalization of a small set. A Proper class is a class which is not a set. A Subclass generalizes a subset. A mapping between classes is a Class function.
Foundation-agnostic usage
We often use the word class in foundation-agnostic contexts. The appropriate interpretations are then:
- In a theory like
one may treat a class indirectly as a predicate ranging over sets and possibly urelements and we say . - In an extension such as
, a class becomes an object in its own right which largely supersedes the notion of a set, with a set becoming a class which is contained in some class. Classhood of is denoted by . Again, classes are taken to satisfy the Axiom of Extensionality - In
a -class is a subset of . - Similarly, in a Type theory with universes a class is the same as an h-set.
#state/develop | #lang/en | #SemBr