Dimitris Tsementzis
unread,Apr 29, 2015, 3:01:48 PM4/29/15Sign in to reply to author
Sign in to forward
You do not have permission to delete messages in this group
Sign in to report message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to Michael Shulman, Thomas Streicher, Bas Spitters, homotopytypetheory
>> [T]he complaint is about postulating axioms without
>> computational meaning as e.g. UA
>> axioms
If the complaint is only about postulating axioms without computational meaning (a.g. UA) then the reliance on such "types and terms" in HoTT/UF could hardly be called "excessive" could it? Furthermore, I don't see how, as Mike suggests, this would be a complaint against HoTT/UF being a foundation at all. It seems merely to be a complaint that it is not a foundation of a certain kind, namely one in which every axiom has computational meaning.
So I think perhaps what Rubio is really referring to is the lack of something like a "W-type for HITs" ("incomplete specification of higher inductive types" as he says in the beginning of the quoted sentence) which would make all of them exist axiomatically "by construction" rather than having to state each one separately as an extra "axiom" of the system every time. This is the only way I can make sense of his use of the word "excessive". I'm still not sure how this fact alone provides a good argument that HoTT/UF should not be considered a foundation of mathematics at all (and even so the argument would only apply to MLTT+UA+HITs not to MLTT+UA.) No-one, surely, wants to claim that variants of MLTT without W-types are automatically not to be thought of as foundations of mathematics for that reason alone - right? But perhaps the fact that such a "W-type for HITs" has not even been defined as a *possible* addition to the system makes the situation different. The worry/argument would then boil down to something like this: "There is currently no way to internalize in the syntax all the constructions that take place in the HoTT book (HITs in particular) in the same way that inductive types can be internalized in the syntax by W-types. Therefore HoTT/UF (as described in the HoTT book) cannot yet be called a foundation of mathematics."
It's hard to come up with a classical analogue of the current situation with HoTT/UF and HITs in order to see if this argument is any good. Perhaps the following is somewhat analogous (though historically a bit inaccurate): In defining categories of sheaves, presheaves etc. in algebraic geometry people were doing all sorts of constructions in set theory whose precise syntactic internalization in (possible extensions of) ZF(C) was unclear. Several solutions were then invented (e.g. Grothendieck universes, inaccessibles etc.) to fix this. But no-one ever doubted that ZF(C) was a foundation for mathematics because it did not come with a pre-packaged solution to the problem of internalizing all of Grothedieck's algebraic geometry. No-one ever said: until we find a way to add axioms to ZF(C) sufficient to express all of Grothendieck's mathematics it is premature to consider ZF(C) a foundation for mathematics. Thinking like this, Rubio's argument seems too strong. An important disanalogy with the current situation, however, is that HITs are constructions being carried out syntactically (though not internally) to begin with. On the other hand, an important analogy with the current situation is that the study of HITs is motivated primarily by mathematical and not metamathematical reasons.
Another possible classical analogue of Rubio's argument could be: ZF is not a foundation of mathematics if we allow ourselves to use some kind of choice principle without encoding all possible choice principles in the syntax in a uniform way (e.g. by the Axiom of Choice, giving us ZFC.) This does not sound right at all.
In trying to come up with analogies, I'm no longer convinced that there's a good argument to be made at all along those lines, if this is indeed what Rubio had in mind. But perhaps the situation with HITs in HoTT/UF is in some sense "unprecedented".
Dimitris