Logic Colloquium 2008
Jaap van Oosten Geometric Aspects of the Effective Topos
The effective topos, discovered by Martin Hyland in 1979, is a generalization to full higher-order type theory of Kleene's realizability interpretation of 1945. It is one coherent mathematical universe in which also recursive analysis, in the words of Hyland, ``finds its natural home''. Moreover, various classically inconsistent theories which did not originate in recursive interpretations of mathematics have been shown to admit models in the effective topos, such as synthetic domain theory, algebraically compact categories and Aczel's Constructive Set Theory (augmented with several nonclassical axioms). In this talk, we shall explore to what extent constructions known from abstract homotopy theory can be performed in the effective topos, and which properties of the category of simplicial sets find analogues in it.