LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
4.00pm, Tuesday 15th July 1997

Title: Universes in Type Theory

Speaker: Anton Setzer (University of Munich, Germany)

In logic we often have to distinguish between large and small objects: the category of all small categories is a large category, the collection of of all (small) sets is a (large) class, etc. Whereas in impredicative type theory we usually only need to distinguish between some global levels like terms vs. types vs. kinds, in predicative theories we cannot internalize large objects that easily and therefore have to introduce a more fine structure. A universe is a separation of the objects of a structure into small objects, those which are in the universe, and the large objects, for instance the universe itself. Various hierarchies of universes have been studied: the finitely nested universes, E. Palmgren's universe operator and super universe, the Mahlo-universe and, most recently, the $\Pi_n$-reflecting universes. We will give an overview over these constructions and report on, what is known about them.