A significant result in set theory was shown by Cohen when he showed that the continuum hypothesis was independent of ZFC using a new technique called forcing. In Topos theory, this result has a new geometric interpretation: the sheaf for the dense topology on the poset of finite approximations on the 'impossible monic' form a new model of sets where this monic is actually there.
Now, presumably Gödel's incompleteness theorem remains valid for typed intuitionistic higher-order logic; such a logic is the internal logic of a topos.
Is there a categorical proof of Gödel's theorem in Topos theory? Does Gödel's theorem say anything geometric or throw new light on the theorem when interpreted in a topos?