The terms "essential" and "concrete" used in the question can be subjected to a variety of interpretations. Yet, I believe that a legitimate answer is provided by the construction of well-adapted topos models of synthetic differential geometry. In order to obtain a sufficiently strong semantics of higher order intuitionistic proofs of various theorems of differential geometry (and functional analysis), it is necessary to move from using presheaves over (the opposite category of) the category of (suitably restricted) rings of smooth functions (over smooth manifolds) to using Grothendieck toposes with subcanonical Grothendieck topology over such sites. In particular, to name something that can be considered as a very concrete result: a construction of a Basel topos, with both invertible and nilpotent infinitesimals, providing a higher order intuitionistic model of infinitesimal analysis with forcing, admitting not only a full and faithful embedding of the Frölicher–Kriegl convenient setting for smooth analysis, but also some elements of the theory of distributions (e.g., the real line version of the Sochocki–Plemelj formula). The main point here is: in many cases the intuitionistic proofs provide a discovery of a new mathematical structure, since they require explicit constructions instead of using axiom of choice or excluded middle. Naturally, it is much harder to perform them, and so this territory is still vastly underexplored. For a detailed account see: Moerdijk I., Reyes G.E., 1991, "Models for smooth infinitesimal analysis", Springer, Berlin.

16more comments