[boxfire]

> 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)

[creata]

You'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_Y...

[1]: http://math.andrej.com/2016/10/10/five-stages-of-accepting-c...

[Ericson2314]

Andreij Bauer is one of those HoTT people, so this is quite tongue-in-cheek.

[mjw1007]

For the avoidance of doubt: Andrej Bauer is himself very much one of those crazy HoTT people.