Set Theory

Wikipedia nLab

Contents

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

(P : A → U) (a : A)(isprop(P(a)), b, c : P(a)) → _ : 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)

(−1)-type_U_i → (−1)-type_U_[i + 1].Ω ≡ 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‖.

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

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.

Images

Quotients

Definition (effective)

Set is a ΠW-pretopos

Cardinal Numbers

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

Cardinal Addition

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

Ordinal Numbers

Wikipedia nLabisset(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)

  • (a < b)(f(a) < f(b)),
  • (a : A) (b : B)(b < f(a)) → ‖(a_0 : A) × (a_0 < a) × (f(a_0) = b)).

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

Theorem

References