A discussion on the homotopytypetheory mailing list prompted me to write this short note. Apparently a mistaken belief has gone viral among certain mathematicians that Univalent foundations is somehow limited to constructive mathematics. This is false. Let me be perfectly clear:

*Univalent foundations subsume classical mathematics!*

The next time you hear someone having doubts about this point, please refer them to this post. A more detailed explanation follows.

Continue reading Univalent foundations subsume classical mathematics