notifications

Set Theory

Wikipedia nLab

0-Types

'Set'.

isset(A) ≑ (x, y : A) β†’ (p, q : x = y) β†’ (p = q).isset(𝟏) (by this and this).isset(𝟎) (by the induction principle for 0).isset(β„•) (see this).

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