4 ms·
> Correct me if I'm wrong but I think that it is really only useful for helping prove theorems in homotopy theory, rather than being more generally useful for o
by alimw 4y ago
> Correct me if I'm wrong but I think that it is really only useful for helping prove theorems in homotopy theory, rather than being more generally useful for other kinds of math.
It seems a little immoral to select a foundation according to how "useful for helping prove theorems" it is...
- edflsafoiewq 4y agoWhat on earth else would you select it for?
- alimw 4y agoUnfortunately I can't find the link but somewhere out there I've seen one you'd like; a radically helpful theorem prover that advertises itself as the quickest and easiest way to prove anything. The joke is that everything is true. For those in this thread who are interested in HoTT and looking for a way in, I'll point out this series of online lectures (+ discord etc. in fact a school) beginning very soon and seemingly designed to provide that introduction. https://uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html https://uwo.ca/math/faculty/kapulkin/seminars/hottest_summer...