Abstract. Martin-Löf's partial type theory, i.e. type theory with a fixed point operator, is extended with universes and given a domain-theoretic interpretation using Scott's information systems. The dependent types are interpreted as monotone families (parametrizations) of information systems and elements as relativized approximable mappings. Universes are interpreted as fixed points of the continuous operators (on the class of parametrizations) that are induced by the introduction rules for universes. Partial type theory has a rich type structure. In fact, as is shown elsewhere, Martin-Löf's inconsistent type theory, Type:Type, is definable in it. However, in this paper we give a direct interpretation of (an extension of) Type:Type as an application of the domain-theoretic method of solving type universe equations introduced here.
Erik Palmgren, March 9, 1999.