Timothy 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. For instance, is Blakers-Massey theorem advanced enough to count as real math?

• C-CoRN library, skim the README or see this paper for a humane summary of what is in it.

• UnitMath library, intitiated by the late Vladimir Voevodsky, browse this folder to get a feel for what is in it.

The moral of the story is that the folk tales that mathematicians tell about how choice-free mathematics is completely different, or even impoverished beyond recognition, are just folk tales. Of course, one has to be a bit more careful, but that is always the case when we generalize, as new phenomena arise.

Timothy 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. For instance, is Blakers-Massey theorem advanced enough to count as real math?

• C-CoRN library, skim the README or see this paper for a humane summary of what is in it.

• UniMath library, inititiated by the late Vladimir Voevodsky, browse this folder to get a feel for what is in it.

The moral of the story is that the folk tales that mathematicians tell about how choice-free mathematics is completely different, or even impoverished beyond recognition, are just folk tales. Of course, one has to be a bit more careful, but that is always the case when we generalize, as new phenomena arise.

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. For instance, is Blakers-Massey theorem advanced enough to count as real math?

• C-CoRN library, skim the README or see this paper for a humane summary of what is in it.

• UnitMath library, intitiated by the late Vladimir Voevodsky, browse this folder 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.

Timothy 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. For instance, is Blakers-Massey theorem advanced enough to count as real math?

• C-CoRN library, skim the README or see this paper for a humane summary of what is in it.

• UnitMath library, intitiated by the late Vladimir Voevodsky, browse this folder to get a feel for what is in it.

The moral of the story is that the folk tales that mathematicians tell about how choice-free mathematics is completely different, or even impoverished beyond recognition, are just folk tales. Of course, one has to be a bit more careful, but that is always the case when we generalize, as new phenomena arise.