Set Theory

0-Types

'Set'.

() () () ()

isset (𝟏) (by type theory#𝟏 and homotopy type theory#𝟏).

isset (𝟎) (by the induction principle for 0).

isset (ℕ) (see homotopy type theory#ℕ).

1-Types

() () () () ()

Lemma

() ()

Example

isset (U) → 0.

(−1)-Types

'Mere proposition'.

isprop (A) ≡ (x, y : A) → x = y.

Lemma

isprop(A) × (a_0 : A) → (A ≃ 𝟏). ∵ f(a : A) ≡ *, g(x : 𝟏) ≡ a_0. isprop(𝟏).

Lemma

_ : isprop (A), _ : isprop (B), _ : A → B, _ : B → A → _ : A ≃ B.

() ()

Lemma

() ()

Lemma

(())

(())

Remark

(())

Classical vs. Intuitionistic Logic

law of excluded middle

(A : U) → isprop (A) → A + ¬A.

law of double negation

() () ()

Decidable

1) A + ¬A. 2) (a : A) → B(a) + ¬B(a). (decidable equality)(a, b : A) → (a = b) + ¬(a = b).

Subsets and Propositional Resizing

'Predicate', 'property'.

() ()

() (() ())

Subuniverses

\begin{matrix} Set_U ≡ & ( & A : U & ) & × isset & ( & A & ) & , \\ Prop_U ≡ & ( & A : U & ) & × isprop & ( & A & ) & . \end{matrix}

(−1)-Truncation

'Propositional truncation', 'bracket type' or 'squash type'.

a : A ⊢ |a| : ‖A‖, x, y : ‖A‖ ⊢ x = y.

Lemma

(P : A → U) (a : A) → (isprop (P (a)), b, c : P (a)) → _ : b = c.

Subtype

() () (()) () () () () () () ()

Axiom (Propositional Resizing)

(−1) -type_U_i → (−1) -type_U_[i + 1].

Ω ≡ Prop_[U_0].

Power Set

() ()

The Logic of Mere Propositions

Example

\begin{matrix} ( & ( & a : A & ) & → isprop & ( & B & ( & a & ) & ) & ) & → isprop & ( & ( & a : A & ) & → B & ( & a & ) & ) & . \\ isprop & ( & A → 𝟎 & ) & . \end{matrix}

Definition

\begin{matrix} ( & a : A & ) & × P & ( & a & ) & ∩ & ( & a : A & ) & × Q & ( & a & ) & ≡ & ( & a : A & ) & × P & ( & a & ) & × Q & ( & x & ) & , \\ ( & a : A & ) & × P & ( & a & ) & ∪ & ( & a : A & ) & × Q & ( & a & ) & ≡ & ( & a : A & ) & × ‖P & ( & a & ) & + Q & ( & x & ) & ‖, \\ A \ & ( & a : A & ) & × P & ( & a & ) & ≡ & ( & a : A & ) & × & ( & P & ( & a & ) & → 𝟎 & ) & . \end{matrix}

Axiom of Choice

(A : X → U) P : (x : X) → A (x) → U

isset(X),
(x : X) → isset(A(x)),
(x : X) → (a : A(x)) → P(x, a) is a mere prop.

(() (()) ()) (() ()) () (())

Lemma

() (()) (() ()) () ()

Remark

(() ()) () ()

Principle of Unique Choice

Lemma

P is a mere proposition, P ≃ ‖P‖.

Corollary

When are propositions truncated?

When A and B are mutually exclusive ((A × B) → 𝟎), A + B ≃ ‖A + B‖.

Contractibility

'Contractible type'.

Definition

'contractible', or a 'singleton'.

() () () ()

Lemma

iscontr (A) ⇔ isprop (A) and a : A ⇔ A ≃ 𝟏.

Lemma

()

Corollary

() (())

Lemma

B : A → U | ((a : A) → (B (a) ≃ 𝟏)) → ((a : A) → B (a)) ≃ 𝟏.

() () ()

Retraction and Section

() ((()))

then we say that B is a retract of A.

Lemma

() ((())) () ()

Lemma

(A : U) (a_0 : A) → ((a : A) × (a_0 = a)) ≃ 𝟏.

Lemma

B : A → U | \begin{matrix} ( & ( & a : A & ) & → & ( & B & ( & a & ) & ≃ 𝟏 & ) & ) & → & ( & ( & a : A & ) & × B & ( & a & ) & ) & ≃ A. \\ ( & A ≃ 𝟏 & ) & × & ( & a_0 : A & ) & → & ( & ( & a : A & ) & × B & ( & a & ) & ) & ≃ B & ( & a_0 & ) & . \end{matrix}

Lemma

() () ()

Exercises

Exercise 3.1

() () ()

Exercise 3.2

() () ()

Exercise 3.3

(() () (())) (() ())

Exercise 3.4

() ()

Exercise 3.5

() (())

Exercise 3.6

() (())

Exercise 3.7

() () (()) ()

The Category of Sets

Limits and Colimits

(() ()) (() (()))

Pullback.

() () (() ())

Set is a complete category.

Since sets are closed under + and contain 0, Set has finite coproducts. Similarly, since (a : A) × B(a) is a set whenever A and each B(a) are, it yields a coproduct of the family B in Set.

pushouts exist in n-types, which includes Set in particular. Thus, Set is also cocomplete.

Images

Quotients

Definition (effective)

Set is a ΠW-pretopos

Cardinal Numbers

Card ≡ ‖Set‖_0. isset (Card) . cardinality (A) ≡ |A|_0.

Cardinal Addition

|A|_0 + |B|_0 ≡ |A + B|_0, (- + -) : Card → Card → Card.

Ordinal Numbers

isset (A) ⊢ (- < -) : A → A → (−1) -type.

Definition (well-founded)

A binary relation < on a set A is well-founded if every element of A is accessible. The point of well-foundedness is that for P : A → U, we can use the induction principle of acc to conclude (a : A) → acc(a) → P(a), and then apply well-foundedness to conclude (a : A) → P(a). In other words, if from (b : A) → (b < a) → P(b) we can prove P(a), then (a : A) → P(a). This is called well-founded induction.

Example

() () () () (()) (())

Well-foundedness allows us to define functions by recursion and prove statements by induction, such as for instance the following.

Lemma

g : 𝒫 (B) → B |

Definition (extensional)

() () () () ()

Theorem

The type of extensional well-founded relations is a set.

Definition (simulation)

$() (() ())$
$() () (()) () () (()))$

Lemma

Any simulation is injective.

Corollary

() () (()) () () (())

initial segment

Theorem

References

Institute for Advanced Study. Homotopy Type Theory: Univalent Foundations of Mathematics. 2013.

Set Theory

Contents

0-Types

1-Types

Lemma

Example

(−1)-Types

Lemma

Lemma

Lemma

Lemma

Remark

Classical vs. Intuitionistic Logic

Decidable

Subsets and Propositional Resizing

Subuniverses

(−1)-Truncation

Lemma

Subtype

Axiom (Propositional Resizing)

Power Set

The Logic of Mere Propositions

Example

Definition

Axiom of Choice

Lemma

Remark

Principle of Unique Choice

Lemma

Corollary

When are propositions truncated?

Contractibility

Definition

Lemma

Lemma

Corollary

Lemma

Retraction and Section

Lemma

Lemma

Lemma

Lemma

Exercises

Exercise 3.1

Exercise 3.2

Exercise 3.3

Exercise 3.4

Exercise 3.5

Exercise 3.6

Exercise 3.7

The Category of Sets

Limits and Colimits

Images

Quotients

Definition (effective)

Set is a ΠW-pretopos

Cardinal Numbers

Cardinal Addition

Ordinal Numbers

Definition (well-founded)

Example

Lemma

Definition (extensional)

Theorem

Definition (simulation)

Lemma

Corollary

Theorem

References