cardinal numbers in the introduction about book HOT 5 OPEN

from book.

from book.

How about this:we canobtain such represen-tatives in a natural way by truncating the universe.

For what it's worth I don't really find this to be an acceptable alternative. The special named type-theoretic universes in most type theories aren't a semantically defined class; they're just particular types that have been selected syntactically to be called universes and are assumed to have the required closure properties. There's nothing in most type theories that prevents the existence of a type in U_1 that codes what by rights should be a proper sub-universe of U_0 but which isn't 'officially' a universe. So given this, why would it be any less natural for a set theory to add a special class of explicitly named inaccessible sets?

from book.

Also the word "representatives" is perhaps a bit misleading to use at all because with this approach we are not selecting canonical "representatives of equivalence classes" for isomorphism of sets but defining a notion of "cardinal number" that doesn't need such representatives.

The way I see it, the mathematical points are:

1. In HoTT, the naturally-defined "type of well-ordered sets" is already a set (in the next universe) and contains exactly one element of each isomorphism class, so we can also call it "the type of ordinal numbers" without needing to specify canonical representatives of well-ordered sets like von Neumann ordinals. However, I think this doesn't really pertain at all to constructivity, which is the point of this section of the introduction, since von Neumann ordinals aren't really a place where constructivity makes things more difficult in set theory: the constructive theory of von Neumann ordinals is fairly well-developed and unproblematic, we just have to use the correct notion of well-foundedness.
2. In HoTT, the 0-truncation of a universe acts as a type of cardinal numbers in that universe. In set theory one usually defines cardinal numbers to be initial ordinals (which requires AC) or using Scott's trick (which requires the axiom of foundation) -- and there are other methods that require less, though still something -- but one could also stipulate a tower of universes like in type theory and obtain a notion of cardinal number in some universe by quotienting the universe by equinumerosity. So the difference between HoTT and set theory here is (1) the use of specified universes, which is standard even in non-univalent type theory and could also be done in set theory, although it isn't usually, and (2) the fact that writing down the 0-truncation doesn't refer explicitly to equinumerosity since that was built into the identity types by univalence.

Do we agree on that, and the question is just what to say in the introduction that is concise and correct?

from book.

Incidentally, Peter Aczel has a paper in which he introduced a couple of specific constructive set theories with explicitly named universes:

Aczel, P. (1999). On Relating Type Theories and Set Theories. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds) Types for Proofs and Programs. TYPES 1998. Lecture Notes in Computer Science, vol 1657. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48167-2_1

from book.