4 ms·
> But who's going to work without AC (other than crazy HoTT people)? Yeah... Those crazy HoTT people, trying to actualize the goal of putting mathematics on an
by boxfire 5y ago
> But who's going to work without AC (other than crazy HoTT people)?
Yeah... Those crazy HoTT people, trying to actualize the goal of putting mathematics on an actually firm foundation and removing the rest of the gobblygook handwaved into the religion of math as opposed to the pure logic it represents...
Also you can use HoTT WITH AC / law of excluded middle... It's just not there by default and there are some really nice things you get without it, so it's pretty much only the lazy crutch of mathematics since forever. If you see proof via excluded middle, consider it a code smell (and recall by the Curry-Howard correspondence the proof is essentially code)
- Ericson2314 5y agoAndreij Bauer is one of those HoTT people, so this is quite tongue-in-cheek.
- creata 5y agoYou're exaggerating the significance of HoTT. Mathematics is already on a pretty firm foundation. And I somehow doubt Bauer meant any ill intent with that line...[0][1] [0]: https://en.wikipedia.org/wiki/Homotopy_type_theory#Special_Year_on_Univalent_Foundations_of_Mathematics https://en.wikipedia.org/wiki/Homotopy_type_theory#Special_Y... [1]: http://math.andrej.com/2016/10/10/five-stages-of-accepting-constructive-mathematics/ http://math.andrej.com/2016/10/10/five-stages-of-accepting-c...
- mjw1007 5y agoFor the avoidance of doubt: Andrej Bauer is himself very much one of those crazy HoTT people.
- deleted 5y ago[deleted]