Sheaves and intuitionistic mathematics

This will be an introductory talk about the interplay between
Grothendieck toposes and intuitionistic mathematics.  It is possible
to construct natural models for intuitionistic principles of
mathematics using topos theory, while conversely, one can prove
structure theorems for toposes using "synthetic" intuitionistic
reasoning inside a topos. Examples of both phenomena will be given.