cardinal numbers in the introduction

[mikeshulman]

James Hanson has pointed out that this comment in the introduction:

In set theory, various circumlocutions are required to obtain notions of “cardinal num-
ber” and “ordinal number” which canonically represent isomorphism classes of sets and
well-ordered sets, respectively — possibly involving the axiom of choice or the axiom of
foundation. But with univalence and higher inductive types, we can obtain such represen-
tatives directly by truncating the universe.

is somewhat misleading, because if a set theory has as many universes as type theory does one can do something similar to obtain a more direct notion of cardinal number by simply quotienting a universe by the equivalence relation of equinumerosity. This is relative to the universe, of course, but so is the type-theoretic notion. So what's added by HoTT is not really the avoidance of AC/AF but just the fact that we can simply truncate the universe, referring to its intrinsic notion of equality and making it an -hset, rather than having to choose the appropriate equivalence relation.

I don't have a rewording to suggest at this time, and I'm not sure whether this is an allowed "first-edition change" either. Thoughts?

[martinescardo]

A thought, for both this and the previous message, is that there shouldn't be anything that upsets set theorists for unnecessary reasons. Hence I vote for this to be a "first-edition change". We should fix wrong claims outside HoTT/UF if we want HoTT/UF to be taken seriously.

[awodey]

How about this:we canobtain such represen-tatives in a natural way  by truncating the universe.Steve On Jun 14, 2024, at 18:24, Mike Shulman ***@***.***> wrote: James Hanson has pointed out that this comment in the introduction: In set theory, various circumlocutions are required to obtain notions of “cardinal num- ber” and “ordinal number” which canonically represent isomorphism classes of sets and well-ordered sets, respectively — possibly involving the axiom of choice or the axiom of foundation. But with univalence and higher inductive types, we can obtain such represen- tatives directly by truncating the universe. is somewhat misleading, because if a set theory has as many universes as type theory does one can do something similar to obtain a more direct notion of cardinal number by simply quotienting a universe by the equivalence relation of equinumerosity. This is relative to the universe, of course, but so is the type-theoretic notion. So what's added by HoTT is not really the avoidance of AC/AF but just the fact that we can simply truncate the universe, referring to its intrinsic notion of equality and making it an -hset, rather than having to choose the appropriate equivalence relation. I don't have a rewording to suggest at this time, and I'm not sure whether this is an allowed "first-edition change" either. Thoughts? —Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[James-Hanson]

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?

[mikeshulman]

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?

[James-Hanson]

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