Per Martin-Löf (Stockholm) Topos theory and type theory Abstract: My purpose is to relate type theory to topos theory by taking the concept of model of type theory to be the counterpart of the notion of elementary topos. Inductive and projective limits of comma (or slice) models of type theory will be considered. The former correspond to the filter quotients of topos theory.