MathSciNet review of the HoTT book
0 views
Skip to first unread message
Bas Spitters
Apr 28, 2015, 9:04:31 AM4/28/15
to homotopytypetheory
Review of our book by Julio Rubio.
Julio (https://esus.unirioja.es/psycotrip/) is an expert on computable
algebraic topology and one of the main implementors of the Kenzo
system.
http://www.ams.org/mathscinet/search/publdoc.html?pg1=INDI&s1=1063327&yrop=eq&dr=pubyear&arg3=2013
Julio (https://esus.unirioja.es/psycotrip/) is an expert on computable
algebraic topology and one of the main implementors of the Kenzo
system.
http://www.ams.org/mathscinet/search/publdoc.html?pg1=INDI&s1=1063327&yrop=eq&dr=pubyear&arg3=2013
Michael Shulman
Apr 28, 2015, 1:32:57 PM4/28/15
to Bas Spitters, homotopytypetheory
Nice!
Of course, classical algebraic topologists use the word "compute" to
mean "prove is equal to", despite that computability theorists might
prefer to reserve it for cases in which there is "an automated
procedure" to find such a group. Perhaps we ought to add some
clarification to the book about the meaning of that word.
Some of his other criticisms are reasonably justified, but I'm also
puzzled by the claim that the lack of canonicity and presence of
axioms cast any doubt on whether HoTT/UF is a foundation for
mathematics. ZFC lacks any sort of canonicity and consists entirely
of axioms, but it is surely a foundation for mathematics if anything
is. Am I misunderstanding his point?
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
Of course, classical algebraic topologists use the word "compute" to
mean "prove is equal to", despite that computability theorists might
prefer to reserve it for cases in which there is "an automated
procedure" to find such a group. Perhaps we ought to add some
clarification to the book about the meaning of that word.
Some of his other criticisms are reasonably justified, but I'm also
puzzled by the claim that the lack of canonicity and presence of
axioms cast any doubt on whether HoTT/UF is a foundation for
mathematics. ZFC lacks any sort of canonicity and consists entirely
of axioms, but it is surely a foundation for mathematics if anything
is. Am I misunderstanding his point?
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
Bas Spitters
Apr 29, 2015, 5:12:47 AM4/29/15
to Michael Shulman, homotopytypetheory
I am guessing that Julio is contrasting HoTT/UF with MLTT here, not with ZFC.
Michael Shulman
Apr 29, 2015, 9:19:21 AM4/29/15
to Bas Spitters, homotopytypetheory
Sure, but in that case it's not reasonable to cast doubt on whether it
is a foundation for mathematics. Is it?
On Tue, Apr 28, 2015 at 11:49 PM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
> I am guessing that Julio is contrasting HoTT/UF with MLTT here, not with ZFC.
>
> On Tue, Apr 28, 2015 at 7:32 PM, Michael Shulman <shu...@sandiego.edu> wrote:
is a foundation for mathematics. Is it?
On Tue, Apr 28, 2015 at 11:49 PM, Bas Spitters <b.a.w.s...@gmail.com> wrote:
> I am guessing that Julio is contrasting HoTT/UF with MLTT here, not with ZFC.
>
> On Tue, Apr 28, 2015 at 7:32 PM, Michael Shulman <shu...@sandiego.edu> wrote:
Thomas Streicher
Apr 29, 2015, 1:07:40 PM4/29/15
to Michael Shulman, Bas Spitters, homotopytypetheory
> Sure, but in that case it's not reasonable to cast doubt on whether it
> is a foundation for mathematics. Is it?
I guess the passage under debate is
> is a foundation for mathematics. Is it?
"the excessive reliance on types and terms whose existence is imposed
by axiom, and not by construction, make it premature to claim that new
foundations of mathematics are described in the book."
as I understand it the complaint is about postulating axioms without
computational meaning as e.g. UA
axioms are ok for usual foundational systems inluding toposes but not
for Martin-Loef Type Theory and alike because their whole purpose is
that everything has computational meaning
this is in contrast with Makki's FOLD where we have a proof irrelevant
logic sitting on top of a model of dependent types. this also was
considered by Peter Aczel and Nicola Gambino
Thomas
Michael Shulman
Apr 29, 2015, 1:09:06 PM4/29/15
to Thomas Streicher, Bas Spitters, homotopytypetheory
Right, I understand that it is something one can complain about. But
I'm saying that that complaint has nothing to do with *whether* the
theory is a foundation for mathematics, just about whether it's the
*sort* of foundation for mathematics that whoever is doing the
complaining *wants* to have.
I'm saying that that complaint has nothing to do with *whether* the
theory is a foundation for mathematics, just about whether it's the
*sort* of foundation for mathematics that whoever is doing the
complaining *wants* to have.
Dimitris Tsementzis
Apr 29, 2015, 3:01:48 PM4/29/15
to Michael Shulman, Thomas Streicher, Bas Spitters, homotopytypetheory
>> [T]he complaint is about postulating axioms without
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
>> 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.
>> axioms
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
Reply all
Reply to author
Forward
0 new messages