Set Theory

Contents
0-Types
'Set'.
1-Types
Lemma
Example
(−1)-Types
'Mere proposition'.
Lemma
isprop(A) × (a_0 : A) → (A ≃ 𝟏). ∵ f(a : A) ≡ *, g(x : 𝟏) ≡ a_0. isprop(𝟏).
Lemma
Lemma
Lemma
Remark
Classical vs. Intuitionistic Logic
law of excluded middle
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
(−1)-Truncation
'Propositional truncation', 'bracket type' or 'squash type'.
Lemma
Subtype
Axiom (Propositional Resizing)
Power Set
The Logic of Mere Propositions
Example
Definition
Axiom of Choice
- 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
Lemma
Corollary
Lemma
Retraction and Section
then we say that B is a retract of A.
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
Pullback.
Set is a complete category.
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

Cardinal Addition
Ordinal Numbers

Definition (well-founded)
Example
Well-foundedness allows us to define functions by recursion and prove statements by induction, such as for instance the following.
Lemma
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