# Set Theory  ## 0-Types

'Set'.

$isset(A) ≡ (x, y : A) → (p, q : x = y) → (p = q).$$isset(𝟏) (by type theory#𝟏 and homotopy type theory#𝟏).$$isset(𝟎) (by the induction principle for 0).$$isset(ℕ) (see homotopy type theory#ℕ).$

## 1-Types

$is−1-type(A) ≡ (x, y : A) → (p, q : x = y) → (r, s : p = q) → (r = s).$

#### Lemma

$isset(A) → is−1-type(A).$

#### 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.$$is(−1)type(𝟎).$

#### Lemma

$isprop(A) → isset(A).$

#### Lemma

$isprop(isprop(A)).$$isprop(isset(A)).$

#### Remark

$isprop(is-equiv(f)).$

## Classical vs. Intuitionistic Logic

law of excluded middle

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

law of double negation

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

### 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'.

$P : A → U | (a : A) × P(a).$$P ⊆ Q ≡ (a : A) → (P(a) → Q(a)).$

### Subuniverses

$Set_U ≡ (A : U) × isset(A),Prop_U ≡ (A : U) × isprop(A).$

## (−1)-Truncation

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

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

#### Lemma

$\left(P : A \to U\right)\left(a : A\right)\to \left(isprop\left(P\left(a\right)\right), b, c : P\left(a\right)\right)\to _ : b = c.$

### Subtype

$(P : A → U) | (a : A) → isprop(P(a)) | (a : A), P(a). 0-type ≡ (A : U), isset(A).(−1)-type ≡ (A : U), isprop(A).$

#### Axiom (Propositional Resizing)

$\left(-1\right)-type_U_i \to \left(-1\right)-type_U_\left[i + 1\right].$$Ω ≡ Prop_[U_0].$

### Power Set

$𝒫(A) ≡ (A → Ω).$

## The Logic of Mere Propositions

### Example

$((a : A) → isprop(B(a))) → isprop((a : A) → B(a)).isprop(A → 𝟎).$

### Definition

$(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) → 𝟎).$

## 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.
$((x : X) → ‖(a : A(x)) × P(x, a)‖) → ‖(g : (x : X) → A(x)) × (x : X) → P(x, g(x))‖.$

#### Lemma

$isset(A) B : A → U isset(B(a)) |((a : A) → ‖B(a)‖) → ‖(a : A) → B(a)‖.$

#### Remark

$((a : A) → ‖B(a)‖) ≃ ‖(a : A) → B(a)‖.$

## Principle of Unique Choice

#### Lemma

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

## 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'.

$iscontr(A) ≡ (a_0 : A) × (a : A) → (a_0 = a).$

#### Lemma

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

#### Lemma

$isprop(A ≃ 𝟏).$

#### Corollary

$(A ≃ 𝟏) → ((A ≃ 𝟏) ≃ 𝟏).$

#### Lemma

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

#### Retraction and Section

$r : A → B s : B → A | ε : (b : B) → (r(s(b)) = b).$

then we say that B is a retract of A.

#### Lemma

$r : A → B s : B → A ε : (b : B) → (r(s(b)) = b) | (A ≃ 𝟏) → (B ≃ 𝟏).$

#### Lemma

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

#### Lemma

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

#### Lemma

$isprop(A) = (a, b : A) → iscontr(a = b).$

## Exercises

### Exercise 3.1

$isset(A ≃ B) × isset(A) → isset(B).$

### Exercise 3.2

$isset(A) × isset(B) → isset(A + B).$

### Exercise 3.3

$(isset(A) × (a : A) → isset(B(a))) → isset((a : A) × B(a)).$

### Exercise 3.4

$isprop(A) = iscontr(A → A).$

### Exercise 3.5

$isprop(A) ≃ (A → iscontr(A)).$

### Exercise 3.6

$isprop(A) → isprop(A + (A → 𝟎)).$

### Exercise 3.7

$isprop(A) × isprop(B) × ((A × B) → 𝟎) → isprop(A + B).$

## The Category of Sets

### Limits and Colimits

$(X → (a : A) → B(a)) ≃ ((a : A) → (X → B(a))).$

Pullback.

$f : A → C, g : B → C | (a : A) × (b : B) × (f(a) = f(b)).$

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.

### Cardinal Numbers  $Card ≡ ‖Set‖_0. isset(Card). cardinality(A) ≡ |A|_0.$

$|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

$For any a : A and f : B(a) → W (x : A) B(x) | w < sup(a, f) ≡ ‖(b : B(a)) × (w = f(b))‖.$

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)

$(a, b : A) → (c : A) → (c < a) = (c < b) → (a = b).$

#### Theorem

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

#### Definition (simulation)

• $\left(a < b\right)\to \left(f\left(a\right)< f\left(b\right)\right),$
• $\left(a : A\right)\left(b : B\right)\to \left(b < f\left(a\right)\right)\to ‖\left(a_0 : A\right)×\left(a_0 < a\right)×\left(f\left(a_0\right)= b\right)‖\right).$

#### Lemma

Any simulation is injective.

#### Corollary

$(a : A) (b : B) → (b < f(a)) → (a_0 : A) × (a_0 < a) × (f(a_0) = b).$

initial segment