@AntonPetrunin, your comment looks pretty extremist to me. Personally, I believe I had a good math school, yet in retospect I wouldn't say that EG, especially stereometry, taught me any "rigor", if you don't identify rigor and bourbakist formalistics. Stereometry was especially a prolonged tedious exercise on calculations in vector calculus. Would you support your PoV by any scientific studies?

I don't really know how sheaves can help in probability theory, but my view of probability doesn't exceed a one-semester undergraduate course. I heard the word about something called "stochastic geometry" which looks like ag/prob mix, and I also assume that anyone can benefit from the study of PDE (e.g. for stochastic motion). If you also count statistical quantum physics as probability, then you should also be interested in things like quantum field theories, and these have a deep relation to sheaves etc, but that looks far too deep for any introduction.

Finally, see Kashiwara, Schapira "Sheaves on manifolds". It discusses a far-reaching generalization of previous themes, with applications to the study of differential equations on manifolds. It's definitely not the book to get a first acquaintance with sheaves, but it gives a nice view of (20 y.old) state of the art.

@TomLaGatta, since I myself am rather far from analysis, I can't be really specific here. I can only give some pointers. Firstly there is the work of Mikio Sato et al. on hyperfunctions, which are a special sort of generalized functions, but are defined and studied via sheaf theory. Secondly, most interesting analytic objects over manifolds (differential forms, tensor fields, connections etc) naturally form sheaves and that part of structure is very important. Any good algebraic complex geometry book will discuss it (e.g. de Rham's theorem).

@TomLaGatta, not exactly true. Synthetic diff. geom. is more about providing a model which allows one to work with infinitely small or infinitely large numbers. In this sense it is like a topos-theoretic version of nonstandard analysis, however it has categorical rather than logical flavor and allows a wider variety of models (e.g. existence of nilpotent infinitesimals and analogies with algebraic geometry).

@François: Thank you! I was thinking specifically about your example. I should have been more careful with a choice of $\mathcal E $, however. I'll elaborate it.

@MurielBech, as far as I remember, the book of M-M contains a detailed enough introduction to logic to understand what classifying topoi are. Even if you never had any formal background inlogic, I'm positive that you know what $\forall$, $\exists$ and $\implies$ mean, or how to write statements formally (any basic analysis or algebra course usually explains it). You don't really need more.

@Steve, is there any logical reason to prefer $=\simeq \simeq$ over $== \simeq$? They both seem to imply each other, although that requires climbing up the univalence ladder, which is a bit unnerving, but looks solid and innocent. The second form $==\simeq$ looks more logically reasonable to me, since we postulate a logical equality between types, and that notion is built-in into type theory, unlike equivalence, which is geometrically and constructively reasonable, but still something extra.

This argument applies basically to any function space you can think of. The reason is that lifting universally topology from stalks to sections is a general sheaf-theoretic construction. It says nothing about defining topology on stalks in the first place. In fact, for that reason people usually move the other way, from topology on sections to topology on stalks.

I don't know if there is any reasonable definition of hom functor for analytic category. The problem is to define complex structure on an infinite-dimensional space.

The topology you describe is just the subspace topology, for the subspace of analytic functions inside the space of all continuous mappings. For all mappings this is called "compact-open topology", and it is indeed natural in the sense of category theory: it is the unique inner hom functor for the category of compactly-generated hausdorff spaces.

I believe the only way to understand the proof of a seemingly trivial theorem is to consider a somewhat similar case where its statement fails. I didn't really understand the first isomorphism theorem for groups until I considered the case of semigroups, where it is formally wrong, and how its statement can be fixed. In the same spirit, calculus proofs of statements about real numbers become much more clear once you start working with p-adic numbers and general metric spaces.

A similar question: mathoverflow.net/questions/85516/…