Frankly we are sick of set theorist traditionalists complaining about type theory, category theory, and other new things without actually bothering to understand them at all.

After multiple decades, it's clear you all are never going to bother to learn our stuff nearly as well as we bothered to learn your stuff. This "debate" is thus completely unproductive without any good agreed-upon foundation to argue form.

(How ironic!)

First, I'm not a set theorist. Second, one of the major motivations for introducing type theory in mathematics was to assist with computer-aided formalization efforts, which has had some success and has a promising future (e.g. the stuff the Lean community has been doing lately). This is great! I'm not complaining at all.

But I do think trumpeting HoTT as a new, improved foundation of mathematics evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics; or even more broadly, the mistaken belief that finding a new foundation of mathematics is an interesting project in the 21st century.

Lurie's comment here explains a bit more: https://mathematicswithoutapologies.wordpress.com/2015/05/13...

(And clearly, Lurie is not some ignorant traditionalist. There's a substantive disagreement that can't be reduced to people not wanting to learn "your stuff.")

I think Mike Shulman's side of the discussion in that thread is also very worth reading, and it's somewhat unfair to (perhaps unintentionally) characterize Lurie as the representative of mathematicians trying to talk sense into the homotopy type theorists. They have a very balanced discussion where each respectfully tries to understand where the other is coming from.

I'm desperately trying to find a lovely philosophical writeup on the different purposes to which a "foundation" is put, and why different foundationalists want those foundations for distinct purposes. I can't seem to hunt it down (Google has become steadily less helpful over time). But the thrust is, I don't think anybody is claiming that HoTT ought to replace ZFC for reverse mathematics in particular; it's "just" a capturing of some pervasive intuitions for concepts at the ground floor of the formalism itself. It takes a perspective that makes grappling with some concepts easier to approach. If you're already a deft hand with a different (very well-established) framework, as Lurie exhibits throughout, maybe it's worth it to keep using the entirely viable tools you have!

There's a well-known line of research into the equiconsistency of set-theoretical and type-theoretical foundations, with many compelling results. So you actually can do "reverse mathematics" of type-theoretical foundations. You aren't losing anything.

You write: "I don't think anybody is claiming that HoTT ought to replace ZFC for reverse mathematics in particular; it's "just" a capturing of some pervasive intuitions for concepts at the ground floor of the formalism itself. It takes a perspective that makes grappling with some concepts easier to approach. If you're already a deft hand with a different (very well-established) framework, maybe it's worth it to keep using the entirely viable tools you have!"

My claim is that "capturing [...] some pervasive intuitions" is not what ZFC is trying to do, or what people in foundations are interested in. Lurie puts the point well when he says a foundation "mean[s] a small number of concepts and assumptions from which the rest of mathematics can be derived." The purposes here are first, to figure out what exactly one must assume to get the rest of mainstream mathematics, and second, to provide a convenient base for doing metamathematics (since the fewer elementary operations/objects you have to reason with, the easier it is to write proofs). Capturing intuitions is completely orthogonal to this endeavor; no one is claiming that set-theoretic translations of everyday mathematical arguments capture the intuitive content of those arguments, because no one one intended ZFC to ever do that in the first place.

Similarly, no one is claiming that handing someone a Turing machine that performs quicksort is a great way to capture the intuition behind quicksort, or explain the algorithm in an understandable way. Turing machines exist as a special-purpose construct to probe the limits of computation, not to reproduce or communicate high-level algoritmhic reasoning. ZFC is like a Turing machine for (meta)math.

I've finally found the article! It is "What do we want a foundation to do?", by Penelope Maddy.

http://www.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want...

I need to reread it myself, but this is the article I was referencing.

Yes, hence my desperate desire to relocate the article on what purposes a foundation may be put to. I say this as neutrally as possible, but I don't think "foundation" has such a singular meaning, and misattributing one "foundation's" goals to be those of another's is probably near the root of your frustration. (It would help my case to find the article; at present I can only relay the ghost of what I took from it.)

HoTT/UF share some purposes of a foundation with ZFC, and not others. Each has purposes the other does not. That's about the safest thing I can say with any faith that I'm doing it justice.

I understand this desire but I think people who believe this should develop a new word or description for what you're attempting to do. See my comment here: https://news.ycombinator.com/item?id=30817964

I want to emphasize I'm not policing semantics just for the sake of being ornery. My reaction is approximately the same as it would be to someone who sends me a graph theory paper and calls it number theory. These distinctions are useful.

Wouldn't it be amusing if a common english word like "foundation", usually referring to the thing on which buildings are constructed, is uniquely reserved for the all the kinds of things on which you can theoretically build all of mathematics, but where none of the people involved are actually trying to do that, and a different word has to be invented for a similar thing, because you got banned out of the club for trying to actually build mathematics on top of it.

Yes, I don't especially disagree; I also think words are most useful when they mean something consistent and precise. Nonetheless, I think it's worth separating the merely terminological disagreement from the deeper semantic disagreement. Please do see the article I found(!) in a cousin comment, by Penelope Maddy. I think it provides a very enlightening perspective on the ways in which ZFC and HoTT/UF both purport to be "foundations" and yet seek to perform different duties.

Thanks. I enjoyed the article you linked. I think the description on page 16 is a good summary of what most people working in foundations take the purpose of foundations to be.

> evinces a misunderstanding of what people who work on foundations actually want out of a foundation of mathematics

This is still gatekeeping who gets to use the word "foundations".

I will go read https://mathematicswithoutapologies.wordpress.com/2015/05/13 but my hopes are not high for a sudden breakthrough.

I'm sorry, but this is not gatekeeping; that term has an established meaning and mathematical history, and corresponds to a productive vein of research going back to Gödel (at least). If you'd like to argue that the study of foundations should be expanded to include the things that HoTT people are interested in, that's one thing. But can we at least agree it does not have a ton of relevance to the questions people have traditionally considered in foundational work? (This is almost by definition if we set it up so that it is mutually interpretable with ZFC.)

Foundations goes back to Cantor and Frege, at least.

Set theorists have made a Whig History of sorts where everything leads to ZFC, but that is just their post-hoc reading of the intellectual history.

We can write Whig Histories too. See https://homepages.inf.ed.ac.uk/wadler/papers/frege/frege.pdf for example.

The fact is both narratives are wrong --- intellectual history is always more pluralistic and meandering than partisans want to admit in hindsight. We, as the underdogs, are ready to admit that. Can you all do the same?

That link talks almost entirely about implications for programming and not mathematics. I recommend the Penelope Maddy article linked in a comment above for a more in-depth discussion of the relevant history and aims of the field. She says things much more clearly than I can.

Yes, my point is "functional programming" and "ZFC" are both not predestined as the inevitable conclusion the ideas preceding them would lead up to.

> going back to Gödel (at least)

See, that is the basic misunderstanding here. Foundations now is a wider topic area than it was in Gödel's day. It's like saying that automobiles run on internal combustion engines in a productive vein of manufacturing going back to Henry Ford (at least). Since those days though, there is this guy Elon who you might like to meet...

I absolutely agree that it's a wider, more sophisticated topic today. This doesn't mean that its main concerns have fundamentally changed. The Maddy article linked in a comment above is extremely clear explanation of this.

I don't see the Maddy link, but anyway try for something written in the current century.

Here, from three years ago: http://www.socsci.uci.edu/~pjmaddy/bio/What%20do%20we%20want...

Thanks, that looks interesting and I'll try to read it. But it appears to mostly be about philosophy, and it doesn't say much about what (mathematical) logicians are doing today.

I did start to read it last night, and finished today.

My understanding is that regular MLTT already can do all the bold things Set theory does, and HFTT (and other developments) aims to make "Proof Checker" better realized (no more "setoid hell").

Ultimately what us CS people care about is a unity of theory and practice. What drew us to computers int the first place was trying to make explicit and tangible ideas that previously were only laboriously communicated from one generation of big brains to the next in the ivory tower.

In that regards, I would say don't even look HoTT or fancy theory developments. Look at Lean, written by a non-type-theorist, and mathlib, written by a non-constructivist.

Lean and Mathilb are plainly plowing a head in ways that no set theory based tool has ever achieved, and covering all the set theory bold points in the process.

Perhaps a new more elegant type theory will replace Lean soon, but honestly I am not even worried about that. The important thing is making math much more accessible without loss of rigor with these tools. If better theories can follow rather than lead that methological revolution, that's fine with me,

As to Category Theory and essential guidance, I have a simple test :). As mathlib (or its sucesssors) matures, let us see how many proofs are refactored to use category theory! I don't want to poo-poo the deeper connections between type theory and cateogory theory, but merely using lots of category theory "library code" in a type theoretic proof assistant not itself designed with explicit reference to category theory is good enough a success story for me.

In conclusion:

- Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care)

  - Regular type theory: *check*
  - HoTT: *check*
  - Set theory: *check*, bonus points for more exotic large cardinals

- Generous Arena, Shared Standard, Meta- mathematical Corral

  - Regular type theory: *check*
  - Set theory: *check*
  - HoTT: WIP because culture shock of weird equality

- Proof Checker:

  - Set theory: *FAIL*
  - Regular type theory: *partial support*, full if we discard all constructive side goals (Lean)
  - HoTT: *check*! (Very recent cubical results

- Essential guidance:

  - Category theory does best, but can use as "library" rather than "language". good enough for now.

I have no objections to claiming success in formalizing mathematics! As I've said, Lean is a big win for type theory.

But formalizing proofs with computers is essentially separate from the rigorous study of the foundations of math (consistency, relative strength of theories, etc.).

You've complained above about set theorists not learning "your stuff," and now it's my turn to complain. You write: 'Risk Assessment: depends how many "large cardinal" type things we want (unlike the 1970s category theorists I personally don't really care).' Large cardinal axioms are essential to the study of the relative consistency strength of mathematical theories. You personally might not care about them, but accommodating them is not a negotiable detail for anything that purports to be useful in the study of foundations.

And yeah, I'm aware the HoTT people have ways around this, fine. My comment is more about the perspective conveyed by your remarks: if you want to have a seat at the table in a discussion about foundational issues, you need to understand basic facts like this. My suspicion is that you might have had bad interactions with set theorists because you don't share certain knowledge they take for granted, and then they get frustrated and end the conversation early. I truly believe that if you went and read a book on set theory and logic, and learned, e.g., wny large cardinals are important, you might understand better where I and other people are coming from.

> Large cardinal axioms are essential to the study of the relative consistency strength of mathematical theories. You personally might not care about them, but accommodating them is not a negotiable detail for anything that purports to be useful in the study of foundations.

It's my understanding that some larger cardinals are needed for foundations, but since the foundations problem was "solved" future work on large cardinals has continued, and that is more "more set theory for set theory's sake", than something needed to accommodate math other "regular" mathematicians are doing.

(With the possible exception of the Grothendiek and Voevodsky line of problems perhaps as the article relates --- separate and ancillary to Voevodsky's desire for a proof checker, and also separate to whether or not categorical methods alone can suffice.)

I actually don't know of type theory having "ways around this". My understanding is that while type theory doesn't appear to face fundamental obstacles here, set theory "has the lead" in making large cardinals (or their equivalents) due to being older, and the type theorists relative disinterest in this area has meant the gap is not closing.

Large cardinals are closely related to what type theorists call "universes". Again, there's a huge amount of equiconsistency and relative consistency results linking type- and set theories. To keep suggesting and implying that type theory cannot possibly be a language for talking about these things is so incredibly careless and obtuse that some people might call it actively misleading.

I'm not sure how that comment is responsive to my post. Sure, type theorists talk about universes, and sure, there are relative consistency results linking type and set theories. My claim is just that large cardinals (or some equivalent concept) are essentially necessary to order theories in consistency strength, so is hard to take a response of the form "it doesn't matter whether HoTT can talk about large cardinals" seriously.