7
$\begingroup$

Univalent foundations has been hyped up as the foundation for mathematics for the future in articles such as this one. Now I've given HoTT a brief look, and at least seen that it appears on the face of it quite different from our usual set theory-first order logic bundle, and I wonder if because of that it will have difficulty gaining traction.

Are the supposed benefits of the theory - apparently better compatibility with proof-checking assistants, and a more "intuitive" idea of equality - likely worth it enough to change the culture of mathematics from sets to types?

I mean, put it this way; if someone, or some group, were to come along tomorrow and write a Bourbaki-esque series covering large swathes of mathematics, starting from perhaps ZFC+Grothendieck Universes, is it likely that that book would quickly become outdated as the mathematical community simply stops basing their work on such a foundation? I understand that in reality most work doesn't actually start from such a foundation, at least not intentionally, but at the moment the fact is that in principle you could hopefully derive that work from such foundations.

I say this because Bourbaki's work quickly became outdated due to the rapid rise of category theory - which Bourbaki's foundations simply could not encompass. If someone actually wanted to write such a treatise again, and not suffer the same fate, would they be better off trying to start from Univalent Foundations, or are the chances of it really lifting off so small that they're better off basing the work on TG set theory as described above?

I know that's a strange way to phrase the question, and I know that to an extent this question is opinion based. If possible I'd mainly like to know how far currently this theory of Univalent Foundations has been accepted by the mathematical community, the relative pros and cons of the theory, and (perhaps based somewhat on opinion, I'll admit) the chances that in, say, 15 years time we'll all be using homotopic types to describe our sets.

$\endgroup$
  • 1
    $\begingroup$ Speculation about the future is not really a good topic for our forum ( but there are other places which it would be good to ask.) $\endgroup$ – rschwieb Jun 6 '15 at 10:42
  • $\begingroup$ Suggestions? I don't really know any websites good for this apart from Reddit and SE. $\endgroup$ – Nethesis Jun 6 '15 at 10:50
  • 4
    $\begingroup$ Popular science, like the article you linked, is by definition popular. It is built on the charisma of people involved, and the artistic freedom in the depiction of the goals and road taken by them. You should, instead, try and read some actual mathematician's opinion about the whole thing. Here are two points to start, one and two. $\endgroup$ – Asaf Karagila Jun 6 '15 at 10:54
  • $\begingroup$ Thank you, is there any website more suited to this question? It appears the community of stack exchange, or just one person perhaps, does not like this kind of question, so I'd prefer to take it down and repost it somewhere that is more suitable. $\endgroup$ – Nethesis Jun 6 '15 at 12:06
  • $\begingroup$ @rschwieb Forgot to put tags. $\endgroup$ – Nethesis Jun 6 '15 at 12:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.