I was reading the Russian translation of Recoltes et Semailles and in the footnote where Grothendieck lists his 12 contributions (including schemes) we find the following lines:
Из этих тем наиболее обширной по своей значимости мне представляется тема топосов, которая осуществляет идею синтеза алгебраической геометрии, топологии и арифметики.
Now, I am no Russian, but I translate this as follows "In my opinion, among these topics the most extensive, in terms of its importance, is the topic of topoi, which implements the idea of synthesis of algebraic geometry, topology and arithmetic."
I am aware that topoi allow us to efficiently package certain pieces of (what I would call) homological algebra. This can be used to establish certain properties of, say, etale cohomology which is useful in arithmetic geometry. A different sort of applications we find in mathematical logic. I am very ignorant of those but I heard there is a cool perspective on forcing using topoi.
The question is: do we have any independent evidence that Grothendieck's estimate of the importance of topoi is accurate?
To clarify, let us consider schemes. They are pretty much necessary if you want to have conceptually clear proofs of, say, Weil conjectures or Mazur's theorem about torsion points. You can try to prove the former in particular cases purely computationally (starting from the defining equations) and you would realize that this problem is difficult. I think it is not unreasonable to expect that you could try something similar with the latter. So, there exist applications of schemes that can be expressed in really simple language and you can convince yourself that trying to prove them in really simple language is not going to fly. This is why I, being a diehard concretist, have immense respect for schemes.
Do we have anything like this for topoi? Are there any applications of topoi that could be "dumbed down" in a similar way?