[oisdk]

> I don't know what your work is, but for the vast majority of people learning HoTT is a complete waste of time.

This is a bizarre thing to say. Learning any mathematics is a complete waste of time.

> gives the (false) impression that it plays some important role in modern mathematics.

What are you talking about?

HoTT is broadly regarded as an exciting and important new area of mathematics; your view is absolutely the minority view. I mean I don't think I'm going to be able to convince you otherwise if you genuinely think that there's "not much content" in HoTT, but there are loads of well-regarded and prominent mathematicians who hold the opposite view to yours.

[spekcular]

Learning mathematics had been incredibly useful to me. If that hasn't been the case for you, I'm sorry.

Your claim that HoTT is "broadly regarded as an exciting and important new area of mathematics" is simply wrong. I suggest talking to a wider variety of mathematicians.

In particular, concerning "well-regarded and prominent mathematicians," Steve Simpson and Harvey Friedman are on record on the Foundations of Mathematics mailing list saying, essentially, that HoTT is a waste of time [0]. The other set theory experts I know agree with them but haven't said so publicly. My impression is that this is a fairly common view in the set theory and foundations community.

Further, Jacob Lurie, who is perhaps the most talented mathematician currently working in higher category theory, has also written he doesn't think highly of it [1].

[0] I can provide links if it you want, but if you search the archive these arguments are easy to find.

[1] View the comments on this blog post: https://mathematicswithoutapologies.wordpress.com/2015/05/13...

[lmm]

> Steve Simpson and Harvey Friedman are on record on the Foundations of Mathematics mailing list saying, essentially, that HoTT is a waste of time [0]. The other set theory experts I know agree with them but haven't said so publicly. My impression is that this is a fairly common view in the set theory and foundations community.

The set theory and foundations community, i.e. the small minority of mathematicians who manage to do effective work on mathematical foundations in ZFC, are precisely the people who we'd expect to be most anti HoTT. It's not necessarily wrong, but it's like concluding that OOP is pointless because you've talked to leading C programming experts.

[oisdk]

> Learning mathematics had been incredibly useful to me.

You have missed my point. We generally don't study only the "useful" things; if we did most of the most important mathematics we have today would have gone unstudied.

> Your claim that HoTT is "broadly regarded as an exciting and important new area of mathematics" is simply wrong.

According to whom? You? You're making an argument about consensus regarding the importance of a given area, but I have seen nothing to indicate that the consensus among mathematicians is in line with your opinion.

> Steve Simpson and Harvey Friedman

They are in the minority. Again, if you're arguing about consensus you can't just point to one or two individuals and say "look! They agree with me!" For goodness' sake, the thread your referring to is well-known partially because it was controversial.

> Jacob Lurie [...] doesn't think highly of it

The content of Lurie's comment and yours are quite different.

[spekcular]

You wrote that "Learning any mathematics is a complete waste of time." There are a variety of ways math could not be a waste of time; practical applications are only one. I don't mean to imply pure mathematics shouldn't be studied, only that I don't believe math was a time waster for me.

> According to whom?

I've talked to a lot of very good mathematicians, including people who've studied and collaborated with people in the HoTT orbit, and people from many other subfields. I'm sorry I don't have exact quantitative data for you.

> They are in the minority. Again, if you're arguing about consensus you can't just point to one or two individuals and say "look! They agree with me!" For goodness' sake, the thread your referring to is well-known partially because it was controversial.

Again, I don't think they're in the minority. Also, there's way more than one relevant thread. That particular fight was litigated over years.

> The content of Lurie's comment and yours are quite different.

He makes many comments on that post. I invite you to read them all. Certainly, I'm not just regurgitating what he says there, but it does provide an example of a top mathematician expressing skepticism about the entire enterprise.

[oisdk]

> You wrote that "Learning any mathematics is a complete waste of time."

Yes, I was being facetious. My point is that by whatever measure pure maths is worth studying (i.e. those measure beyond "practical" applications) also obviously applies to HoTT.

> I've talked to a lot of very good mathematicians

You're an anonymous person on the internet, this is such a strange thing to fall back on. There are pretty standard ways of talking about how well-regarded/important certain subfields are in mathematics, "I've asked around" isn't one of them.

> I'm not just regurgitating what he says there

His comments express a substantially different point to yours. He does not say that HoTT is a waste of time, or that it "doesn't have much content".

[spekcular]

> My point is that by whatever measure pure maths is worth studying (i.e. those measure beyond "practical" applications) also obviously applies to HoTT.

Not all branches of pure mathematics are equally worthy of study. A few are essentially dead for various (good) reasons, for example.

> There are pretty standard ways of talking about how well-regarded/important certain subfields are in mathematics, "I've asked around" isn't one of them.

How should one figure out how well-regarded a subfield of mathematics is if not by asking members of the mathematical community?

> His comments express a substantially different point to yours. He does not say that HoTT is a waste of time, or that it "doesn't have much content".

His comments support the point I intended them to support, which is that Lurie is not a huge fan of HoTT. You made a remark about well-regarded mathematicians, and I gave you comments from a well-regarded mathematician.

[oisdk]

> Not all branches of pure mathematics are equally worthy of study.

Ok? What does this have to do with the point I was making?

My point was, pretty simply, that "usefulness" is not the only thing we consider when deciding whether something is worthy of study. (If it was we wouldn't have touched most of modern pure mathematics.) As a result, your notion that studying HoTT would be a waste of time because it's not "useful" is nonsense.

> How should one figure out how well-regarded a subfield of mathematics is if not by asking members of the mathematical community?

Oh come on, you really don't understand the point I'm making?

When talking about consensus it's not good enough to say "I've talked to a few people and they agree with me". Work on HoTT, measured by any kind of actual metric rather than "people I've spoken to (who I can't name by the way) say it's bad", is broadly well-regarded and seen as important. In terms of research funding, citation/publication metrics, or the opinion of most mathematicians.

> His comments support the point I intended them to support

No they do not. My objection is to you saying:

* That HoTT is a waste of time.

* That HoTT doesn't have much content.

* That HoTT is not broadly regarded by mathematicians as important or exciting.

Please do not move the goalposts.

> You made a remark about well-regarded mathematicians, and I gave you comments from a well-regarded mathematician.

What? I "made a remark" about well-regarded mathematicians? I said, specifically, "there are loads of well-regarded and prominent mathematicians who hold the opposite view to yours".

I also tried to stress that:

> if you're arguing about consensus you can't just point to one or two individuals

Please bear that in mind.