Using the internal logic of a topos it's often possible to derive newer theorems about sheaves from earlier ones about simpler objects, assuming that you can prove the earlier ones constructively. In addition, Barr's Theorem allows one to directly reuse classical results when they have a geometric statement relative to a geometric theory.

How far can you take this? Can scheme-theoretic algebraic geometry can be developed internally in the appropriate topoi, or are there some notions that have inherently extrinsic definitions and proofs?

Using the internal language of toposes in algebraic geometry(rawgit.com/iblech/internal-methods/master/notes.pdf) $\endgroup$ – David Roberts Dec 3 '16 at 7:121more comment