Timoth Chow gave a fine answer in the context of classical mathematics. Here are some further sources for you to ponder. These not only work without choice, but also without excluded middle: * [Homotopy Type Theory: Univalent Foundations of Mathematics](https://homotopytypetheory.org/book/). For instance, is [Blakers-Massey theorem](https://en.wikipedia.org/wiki/Blakers–Massey_theorem) advanced enough to count as real math? * [C-CoRN](https://github.com/coq-community/corn) library, skim the README or see [this paper](https://www.cs.ru.nl/~herman/PUBS/ccorn.pdf) for a humane summary of what is in it. * [UnitMath](https://github.com/UniMath/UniMath) library, intitiated by the late Vladimir Voevodsky, browse [this folder](https://github.com/UniMath/UniMath/tree/master/UniMath) to get a feel for what is in it. The moral of the story is that the folk tales that mathematicians tell about the supremacy of the orthodox foundations are just that, folk tales.