Constructive Zermelo-Fraenkel in Martin-Löf's theory

CZF_in_MLTT.txt

These are the notes used in this video:

https://youtu.be/HT_eFdXKJbs

# Book
"Constructivism in Mathematics - An Introduction" (1988)
by A.S. Troelstra & van Dalen
https://www.amazon.com/Constructivism-Mathematics-121-Introduction-Foundations/dp/0444705066
The Book is printed in 2 Volumes (but with common page numbering),
I found 4 pages of errata online.

## Authors
https://en.wikipedia.org/wiki/Anne_Sjerp_Troelstra
https://en.wikipedia.org/wiki/Dirk_van_Dalen

# MLVi (around p. 618)
TT in this note means a dependently typed (in fact ML) type theory with
universes and W-types, i.e. a notion of "well-founded branching tree" toolings.
Those will be used for recursive definitions and a notion of indexing.
For more,
https://ncatlab.org/nlab/show/W-type
https://en.wikipedia.org/wiki/Inductive_type#W-_and_M-types
and pp. 611-619 in the book.

# CZF (p. 619-)
See literature in
https://gist.github.com/Nikolaj-K/951d44b393a92acc51f915fcb0e31cc2
See also
https://youtu.be/HrN7orXvu9k
https://en.wikipedia.org/wiki/Constructive_set_theory

# Quick note on naive Collection
Naively, sets are collected from the aether:
"X_{P} := all conceivable x such that P(x) holds, where conceivable rules
out that x would violate some other axiom you adopted"

We may suggestively write this as
"X_{P} = {x | P(x)}"

# CZF in MLVi (p. 624-)
## Interpretation
In the interpretation, you already got a (ML) TT with (constructive) types A,
and sets are type A-indexed collections, where the extension of the elements
are defined by a function expression f=\x->t in the TT.
"X_{A,f} := the pair <A, f>, read as the range of f w.r.t. A"

We may suggestively write this as
"X_{A,f} := {f(x) | x:A}"
So sets are effectively ranges of TT-functions.

Equality of sets may be defined recursively by a forall over A
(X_{A,f} == Y_{B,g}) := forall x:A. exists y:B. f(x)==g(y) 
(and vice versa, A<->B)

Membership may be defined by exist over A and comparison using the above equality
(a ∈ X_{A,f}) := exists x:A. a==f(x)

Let P be a suitable dependent type.
And then e.g. the set-theoretical forall can be rolled out to the TT one:
(forall (a ∈ X_{A,f}). P(a)) := forall x:A. P(f(x))


The proof that the equality and membership then fulfills axioms such equivalence
relation for '=='
and, for '∈', axioms such as set theoretical induction, pairing, union,
separation axioms, infinity, etc.
can in this way be transferred to type/term existence.

The question is then also relevant how that plays together with ML levels.
Universal quantification in the set world touches "bigger" types on the TT side.

## Choice
The model also validates countable choice AC_0 and dependent choice DC, i.e.
choice holds over N.
DC proves existence of a sequence given by transfinite recursion of countable
length, with "strong choices" at each step.
(Note: Countable ordinals can still have jumps between infinite sections.)
https://en.wikipedia.org/wiki/Axiom_of_dependent_choice

## Presentation axiom (p. 631)
The book section concludes (on p.632) with the remark that if you add some axioms
concerning the universes on the TT side, then you can validate that every set
(in the interpreted CZF) is the surjective image of a set over which choice
holds (a.k.a. a set that is a "base")

# Note on sets in HoTT
Sets are structure-less types, i.e. like categories where the arrows are all
just identity. See
https://axiomsofchoice.org/babbys_first_hott
https://axiomsofchoice.org/univalence_axiom
https://axiomsofchoice.org/set_._hott
https://axiomsofchoice.org/subset_._hott