# 1.2 Sets, Types, and Universes ## 1.2 Sets, Types, and Universes Mathematics needs a way to say what kind of thing an object is. Before we can prove a statement, define a function, or compare two objects, we need a domain of discourse. Sets, types, and universes provide different ways to organize that domain. A set is a collection of objects, called elements. We write: ```text x ∈ A ``` to mean that `x` is an element of the set `A`. For example: ```text 3 ∈ N -2 ∈ Z 1/2 ∈ Q π ∈ R ``` The set tells us where an object lives. It also tells us what operations and statements are expected to make sense. Addition is defined on natural numbers, integers, rational numbers, real numbers, complex numbers, vectors, matrices, and many other structures, but each setting gives addition a particular meaning. A type plays a similar role, but with a stronger emphasis on formation rules. To say that `x` has type `T` means that `x` is a valid object of kind `T`. ```text x : T ``` This notation is common in type theory, proof assistants, and programming language semantics. Sets and types often behave similarly in informal mathematics. The statement “let `x ∈ R`” and the statement “let `x : R`” both declare that `x` is a real number. But they come from different foundations. | Idea | Set-theoretic view | Type-theoretic view | | -------------- | -------------------------------------------------- | ---------------------------------------- | | Membership | `x ∈ A` | Usually replaced by typing | | Classification | Objects belong to sets | Objects have types | | Equality | Often global | Usually type-sensitive | | Functions | Subsets of products or mappings between sets | Terms transforming one type into another | | Error handling | Ill-formed expressions may still appear informally | Ill-typed expressions are rejected | In set theory, many objects live in one large universe of sets. Numbers, functions, relations, ordered pairs, graphs, and spaces can all be encoded as sets. This gives a uniform foundation. A graph can be represented as a pair of sets. A function can be represented as a set of ordered pairs. A topology can be represented as a set of subsets. In type theory, each object belongs to a type. Expressions are checked against typing rules. A function from natural numbers to real numbers has a type such as: ```text f : N → R ``` This says that `f` accepts a natural number and returns a real number. The expression `f(3)` makes sense if `3 : N`. The expression `f(circle)` makes no sense unless `circle` has type `N`, which it normally does not. This type discipline helps prevent meaningless expressions. It is especially important in formalized mathematics and verified software. Universes solve a size problem. If every collection could be treated as a set of the same kind, paradoxes arise. The classical example is the “set of all sets that do not contain themselves.” To avoid such contradictions, foundations distinguish between levels. A universe is a domain large enough to contain many mathematical objects, but not so large that it contains itself without restriction. In set theory, this appears through cumulative hierarchies. Sets are built in stages. At each stage, we collect subsets of what came before. Larger and larger levels produce more complicated sets. ```text V0, V1, V2, V3, ... ``` The exact formal construction can vary, but the idea is simple: objects are stratified by size or rank. In type theory, universes are often written as: ```text Type 0 Type 1 Type 2 ... ``` A small type may live in `Type 0`. The type of small types may live in `Type 1`. This avoids making one type contain itself in an unrestricted way. | Level | Informal role | | ------------- | --------------------------------------- | | `Type 0` | Ordinary mathematical objects | | `Type 1` | Types whose elements are ordinary types | | `Type 2` | Types of larger type collections | | Higher levels | Further stratification | Universes are usually invisible in ordinary mathematics. A textbook rarely says which universe a group, ring, or topological space belongs to. But the issue becomes important when building foundations, writing proof assistant code, or discussing categories of large objects. For example, the category of all groups is large. Its objects are groups, and each group itself contains a set of elements. If we treat “all groups” as an ordinary set without care, we may run into size problems. Category theory handles this by distinguishing small categories, large categories, and universes. Sets are convenient for extensional reasoning. Two sets are equal when they have the same elements. ```text A = B exactly when every element of A is an element of B, and every element of B is an element of A. ``` Types are convenient for intensional reasoning. The way an object is constructed can matter, and equality may require more structure. In many formal systems, converting between types must be explicit. For example, the natural number `3`, the integer `3`, the rational number `3`, and the real number `3` may be treated as different typed objects connected by coercions. ```text 3 : N 3 : Z 3 : Q 3 : R ``` Informal mathematics often suppresses these distinctions. A proof assistant usually forces them to be specified. This suppression is useful but dangerous. It makes mathematics readable, but it can hide assumptions. When a theorem states that a function is continuous, we must know the topology on the domain and codomain. When a theorem states that a sequence converges, we must know the ambient space. When a theorem states that a matrix is invertible, we must know the field or ring of coefficients. The phrase “let `x` be an object” is incomplete until we know the setting. A good mathematical statement declares enough context for its symbols to be meaningful. For example: ```text Let V be a finite-dimensional vector space over a field k. Let T : V → V be a linear map. ``` This gives the carrier, scalar field, dimension assumption, and structure-preserving map. Later statements about eigenvalues, invariant subspaces, or determinants now have a defined setting. Poorly specified context leads to false or ambiguous claims. The equation: ```text x^2 + 1 = 0 ``` has no solution in the real numbers, but it has two solutions in the complex numbers. The truth of a statement depends on the universe in which it is interpreted. | Statement | Context | Result | | --------------------------------------------------- | ---------------- | --------------- | | `x^2 + 1 = 0` | `x ∈ R` | No solution | | `x^2 + 1 = 0` | `x ∈ C` | Solutions exist | | Every nonzero element has an inverse | Integers | False | | Every nonzero element has an inverse | Rational numbers | True | | Every bounded sequence has a convergent subsequence | Real numbers | True | | Every bounded sequence has a convergent subsequence | Rational numbers | False | The lesson is direct: objects, statements, and proofs live inside a chosen context. Sets, types, and universes are not competing notations only. They represent different attitudes toward mathematical organization. Sets ask: what elements belong to this collection? Types ask: what kind of object is this expression allowed to be? Universes ask: how large is the domain we are quantifying over? A working mathematician often uses all three ideas informally. A formal system forces the distinctions to become precise. The best practice is to write enough context for the reader to know which objects exist, which operations are valid, and which equality relation is being used. Mathematics becomes safer when every symbol has a home.