MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

2 added 161 characters in body

Remark: Several items below refer to the formalism of locales. Although consistent usage of the language of locales allows one to get rid of the axiom of choice in almost all cases, my main reasons for it are purely pragmatic: The formalism of locales allows one to obtain equivariant and family versions of many theorems without any additional effort, as opposed to the formalism of topological spaces (think of Hahn-Banach theorem, for example).

• A general topology textbook written in the language of locales, with no mention of topological spaces.

• Textbooks on commutative algebra and algebraic topology written in the language of locales. In particular, such textbooks can usually avoid mentioning maximal ideals, the axiom of choice, or Zorn's lemma.

• A measure theory textbook written in the language of locales and commutative von Neumann algebras, with no mention of the set-theoretical approach. The textbook should also have a conceptual exposition of Lp-spaces.

• A linear algebra textbook that does not mention coordinates, bases, or matrices.

• A textbook on smooth manifolds that never mentions coordinates, charts, or atlases. Such a textbook should have a conceptual exposition of integration and use supermanifolds consistently whenever it makes sense, e.g., for differential forms.

• Textbooks on algebraic topology and homological algebra written in the language of (∞,1)-categories.

• Higher categories for the working mathematician. This book should contain a lot of examples of higher categories that are actually used in mathematics outside of category theory. (For example, the bicategory of algebras, bimodules, and intertwiners, the tricategory of conformal nets, defects, sectors, and morphisms of sectors etc.)

• A textbook on topological vector spaces (in particular, on locally convex, Banach, and nuclear spaces) written from the categorical viewpoint. For example, such a textbook would define a nuclear morphism as a morphism that can be factorized in a certain way (see a recent paper by Stephan Stolz and Peter Teichner). The textbook should consistently use the language of locales. For example, this allows one to prove Hahn-Banach, Gelfand-Neumark, or Banach-Alaoglu theorems without using the axiom of choice.

Remark: Several items below refer to the formalism of locales. Although consistent usage of the language of locales allows one to get rid of the axiom of choice in almost all cases, my main reasons for it are purely pragmatic: The formalism of locales allows one to obtain equivariant and family versions of many theorems without any additional effort, as opposed to the formalism of topological spaces (think of Hahn-Banach theorem, for example).

• A general topology textbook written in the language of locales, with no mention of topological spaces.

• Textbooks on commutative algebra and algebraic topology written in the language of locales. In particular, such textbooks can usually avoid mentioning maximal ideals, the axiom of choice, or Zorn's lemma.

• A measure theory textbook written in the language of locales and commutative von Neumann algebras, with no mention of the set-theoretical approach. The textbook should also have a conceptual exposition of Lp-spaces.

• A linear algebra textbook that does not mention coordinates, bases, or matrices.

• A textbook on smooth manifolds that never mentions coordinates, charts, or atlases. Such a textbook should have a conceptual exposition of integration and use supermanifolds consistently whenever it makes sense, e.g., for differential forms.

• Textbooks on algebraic topology and homological algebra written in the language of (∞,1)-categories.

• Higher categories for working mathematician. This book should contain a lot of examples of higher categories that are actually used in mathematics outside of category theory.

• A textbook on topological vector spaces (in particular, on locally convex, Banach, and nuclear spaces) written from the categorical viewpoint. For example, such a textbook would define a nuclear morphism as a morphism that can be factorized in a certain way (see a recent paper by Stephan Stolz and Peter Teichner). The textbook should consistently use the language of locales. For example, this allows one to prove Hahn-Banach, Gelfand-Neumark, or Banach-Alaoglu theorems without using the axiom of choice.