6 ms·

I don't have much to say here that I didn't already say above about the meta-mathematical issues. However, about object-level mathematical issues, you write: "I

I don't have much to say here that I didn't already say above about the meta-mathematical issues. However, about object-level mathematical issues, you write: "It is a work in progress and might take some time before bearing substantive fruit, but note that the current alternative is that any student learning higher level mathematics at the level of Lurie's books has to go through a huge amount of foundational material while the ideas themselves may not be intrinsically complicated. Instead, this complexity is an artifact of embedding the theory in current foundations like the SDG example mentioned above." Higher category theory is not the same thing as homotopy type theory. One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. As far as I know, issues of ZFC vs type theory simply do not arise. You can just pick up Higher Topos Theory and start reading, assuming you have a strong background in algebraic topology. The linked article is only about higher category theory and making sure all of its claims are written down in a clear and rigorous fashion to be maximally useful to workers in the field. It has nothing to do with the foundations of mathematics as a whole.

enugu 5y ago
> One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. By foundations here, I didnt mean foundations of mathematics, rather the amount of material a student needs to read to become familiar with the basic definitions of what a space means. We can teach topology to undergrads, can we teach higher categorical notions of space? Even schemes themselves had a daunting reputation some time back, now we have derived stacks which involve infinite categories. > You can just pick up Higher Topos Theory and start reading Yes, but my point, as illustrated in SDG example, was that definitions can be easy or hard depending on which foundations you use. You havent mentioned whether you disagree with this and if you see Kock's book, I think you will agree. When dealing with higher categories, a foundations which uses '=' symbol in a different way, with an equivalence relation(modelled on homotopy equivalence) playing a much more prominent role could make the theory much more natural. Note, that I am not even emphasizing sets vs type theory here, but excluded middle and a good notion of equivalence(and equivalence between equivalences... like in homotopy theory) in the foundations. Maybe a lot of this debate will get dissolved if we just use two different words for 'examining consistency of axioms' and 'naturality of theory as encoded in a given system' instead of using the same word - foundations - for both of them. At the very least if discussions begin with an awareness of this distinct usage, there would be lot less talking past each other. Urs Schreiber makes the same point about naturality here - https://golem.ph.utexas.edu/category/2016/03/foundations_of_mathematics.html https://golem.ph.utexas.edu/category/2016/03/foundations_of_...
- spekcular 5y ago
  1) Yeah, Lurie's books are advanced tracts aimed at specialists in algebraic topology. Of course there are going to be substantial prerequisites. This is sort of inevitable if you want to understand the motivating applications. 2) Why would we ever want to teach higher categorical notions of space to undergraduates? We can barely get them out in four years knowing real analysis and abstract algebra. The next stop would be the basic theory of manifolds, not higher topos theory. 3) I looked at Kock's book (the draft of the CUP book on his website). The definitions are more abstract than the ones I would give to undergrads, and consequently harder for them to understand. The appeal is not clear to me. 4) You don't have to change your foundations (meaning ZFC vs. type theory, etc.) to do higher category theory in a reasonable way. Again, go pick up Lurie's books. The exposition would not really be affected by whether you choose type theory or ZFC for a foundation. Let me know if you think there's a counterexample to this claim. (The exposition probably would be affected if you denied the law of excluded middle, for the worse; luckily Lurie doesn't do that.) 5) Foundations are sort of irrelevant here anyway. The point of ZFC is that you can forget about it when actually doing math. If you're thinking about foundations when reading Lurie's books, you're doing something wrong. (Consider: most mathematicians have zero opinion about foundational questions or concepts because they have no bearing on their day to day work.)

enugu 5y ago

> One does not need to learn anything about the foundations of mathematics to read and understand Lurie's work. By foundations here, I didnt mean foundations of mathematics, rather the amount of material a student needs to read to become familiar with the basic definitions of what a space means. We can teach topology to undergrads, can we teach higher categorical notions of space? Even schemes themselves had a daunting reputation some time back, now we have derived stacks which involve infinite categories. > You can just pick up Higher Topos Theory and start reading Yes, but my point, as illustrated in SDG example, was that definitions can be easy or hard depending on which foundations you use. You havent mentioned whether you disagree with this and if you see Kock's book, I think you will agree. When dealing with higher categories, a foundations which uses '=' symbol in a different way, with an equivalence relation(modelled on homotopy equivalence) playing a much more prominent role could make the theory much more natural. Note, that I am not even emphasizing sets vs type theory here, but excluded middle and a good notion of equivalence(and equivalence between equivalences... like in homotopy theory) in the foundations. Maybe a lot of this debate will get dissolved if we just use two different words for 'examining consistency of axioms' and 'naturality of theory as encoded in a given system' instead of using the same word - foundations - for both of them. At the very least if discussions begin with an awareness of this distinct usage, there would be lot less talking past each other. Urs Schreiber makes the same point about naturality here - https://golem.ph.utexas.edu/category/2016/03/foundations_of_mathematics.html https://golem.ph.utexas.edu/category/2016/03/foundations_of_...

spekcular 5y ago
1) Yeah, Lurie's books are advanced tracts aimed at specialists in algebraic topology. Of course there are going to be substantial prerequisites. This is sort of inevitable if you want to understand the motivating applications. 2) Why would we ever want to teach higher categorical notions of space to undergraduates? We can barely get them out in four years knowing real analysis and abstract algebra. The next stop would be the basic theory of manifolds, not higher topos theory. 3) I looked at Kock's book (the draft of the CUP book on his website). The definitions are more abstract than the ones I would give to undergrads, and consequently harder for them to understand. The appeal is not clear to me. 4) You don't have to change your foundations (meaning ZFC vs. type theory, etc.) to do higher category theory in a reasonable way. Again, go pick up Lurie's books. The exposition would not really be affected by whether you choose type theory or ZFC for a foundation. Let me know if you think there's a counterexample to this claim. (The exposition probably would be affected if you denied the law of excluded middle, for the worse; luckily Lurie doesn't do that.) 5) Foundations are sort of irrelevant here anyway. The point of ZFC is that you can forget about it when actually doing math. If you're thinking about foundations when reading Lurie's books, you're doing something wrong. (Consider: most mathematicians have zero opinion about foundational questions or concepts because they have no bearing on their day to day work.)