Open mikeshulman opened 3 months ago
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.
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: @.***>
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?
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:
Do we agree on that, and the question is just what to say in the introduction that is concise and correct?
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
James Hanson has pointed out that this comment in the introduction:
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?