2.1.1. Sets versus types🔗

The first reflex to unlearn is the set-theoretic one that everything is a set. In set theory ∈ is the single primitive, an object can be a member of many sets, and there is no fixed notion of "the type of x". Type theory inverts this: the primitive is the type, and every term a : α has exactly one type, fixed once and for all.

So what is a set in Lean? It is not a new type. A Set α is a predicate on the already-existing type α -- in fact Set α is definitionally α → Prop -- that carves out some of α's terms. An element of s : Set α therefore still has type α; the set only records which terms of α lie in it, and a ∈ s is just s a.

Three notions are worth keeping firmly apart:

• a type α -- the ambient collection of terms;

• a set s : Set α -- a predicate selecting terms of α, whose elements keep their type α;

• a subtype { x : α // p x } (see Subtypes) -- a genuinely new type, whose terms are pairs of a value and a proof that it satisfies p.

So there is a difference between a set and a type, and it is the one a mathematician must internalize. The rest of this chapter makes it precise: sets as predicates and their operations, when two sets are equal, and finally how to cross the gap -- turning a set back into a type.

2.1.2. Notation and naming conventions🔗

The set-theoretic symbols below are unicode characters typed in VS Code via a backslash escape. Hover over a symbol in the editor to see its input sequence.

2.1.3. Sets are predicates🔗

In Mathlib a set over a type α has type Set α, and Set α is definitionally the function type α → Prop. A set is thus nothing more than a predicate: the term a : α belongs to s : Set α exactly when s a holds, and a ∈ s is notation for precisely that.

Because a set is a predicate, two predicates that hold of exactly the same elements describe the same set -- set equality is extensional. We make this precise just below.

2.1.4. Subset, union, intersection, complement🔗

The usual Boolean operations on sets are all defined pointwise on the underlying predicates, so each unfolds to a familiar logical connective.

2.1.5. Indexed unions and intersections🔗

The binary ∪ and ∩ extend to arbitrary families. Given s : ι → Set α -- a set s i for each index i : ι -- the indexed union ⋃ i, s i and indexed intersection ⋂ i, s i collect members across the whole family.

Set.iUnion.{u, v} {α : Type u} {ι : Sort v} (s : ι → Set α) : Set α
Set.iUnion.{u, v} {α : Type u}
  {ι : Sort v} (s : ι → Set α) : Set α

Set.iInter.{u, v} {α : Type u} {ι : Sort v} (s : ι → Set α) : Set α
Set.iInter.{u, v} {α : Type u}
  {ι : Sort v} (s : ι → Set α) : Set α

As always, membership just unfolds to a quantifier:

A common variant restricts the index to a set a : Set ι rather than the whole index type -- written ⋃ i ∈ a, s i and ⋂ i ∈ a, s i. This is just the indexed operation ranging over the members of a, and membership carries the bound along:

When the family is given not by an index but as a set of sets S : Set (Set α), the same operations are written ⋃₀ S (sUnion) and ⋂₀ S (sInter):

Set.sUnion.{u} {α : Type u} (S : Set (Set α)) : Set α
Set.sUnion.{u} {α : Type u}
  (S : Set (Set α)) : Set α

Set.sInter.{u} {α : Type u} (S : Set (Set α)) : Set α
Set.sInter.{u} {α : Type u}
  (S : Set (Set α)) : Set α

These are exactly the set/indexed suprema and infima of the complete lattice of sets: ⋃ i, s i is iSup s, and ⋃₀ S is sSup S. They are also what σ-algebras are closed under -- a countable union or intersection is just the indexed one over ι = ℕ.

2.1.6. Set equality🔗

Two sets are equal exactly when they have the same members -- the set extensionality principle Set.ext. That this holds at all, and is not merely a definition, is a real foundational fact: since a set is a function into Prop, it rests on the extensionality axioms taken up in the next chapter. Here we simply use it.

2.1.7. From a set back to a type: subtypes and coercion🔗

A set is not a type -- but sometimes you need one, for instance to speak of a function defined only on s, or to sum over its elements. A set can be promoted to a type by coercion: ↥s denotes the subtype { x // x ∈ s } of its members, a genuinely new type whose terms pair an element of α with a proof of membership.

With sets, subtypes, and their relationship to types in hand, we are ready to look at the structures Mathlib builds on top of them.

2.2.1. The universe hierarchy🔗

Part 1 introduced the universe hierarchy as a working tool: Prop = Sort 0, Type = Type 0 = Sort 1, Type u = Sort (u+1), the single rule Sort u : Sort (u + 1), and universe-polymorphism via Type*. Here we record why the absence of Type : Type is not optional. Were Type : Type to hold, one could reproduce Russell's paradox at the level of types -- Girard's paradox -- and thereby prove False. The stratification

is exactly what blocks this, and it is what keeps the whole system consistent. Everything else in this chapter -- the axioms, proof irrelevance, the CIC -- rests on top of it.

-- Under `Type : Type`, σ becomes definable (with the reduction
--   σ (τ t) p  =  t (fun x => p (τ (σ x)))  ), and the rest goes:
def σ (s : U) : Set (Set U) := s U τ

-- Δ is the Russell set `{x | x ∉ x}`; Ω is its diagonal fixpoint.
def Δ : Set U := fun y => ¬ ∀ p : Set U, σ y p → p (τ (σ y))
def Ω : U := τ (fun p => ∀ x : U, σ x p → p x)

-- Every property holding hereditarily along σ holds at Ω:
def lem : ∀ p : Set U, (∀ x : U, σ x p → p x) → p Ω :=
  fun p H => H Ω (fun x => H (τ (σ x)))

-- Feeding `lem` the bad set Δ yields both Δ Ω and ¬ Δ Ω:
theorem girard : False :=
  lem Δ
    (fun x l₂ l₃ => l₃ Δ l₂ (fun p => l₃ (fun y => p (τ (σ y)))))
    (fun p => lem (fun y => p (τ (σ y))))