Introduction

In this paper we study some extensions of the Kleene-Kreisel continuous functionals and show that most of the constructions and results, in particular the crucial density theorem, carry over from finite to dependent and transfinite types. Following an approach of Ershov we define the continuous functionals as the total elements in a hierarchy of Ershov-Scott-domains of partial continuous functionals. In this setting the density theorem says that the total functionals are topologically dense in the partial ones, i.e. every finite (compact) functional has a total extension. We will extend this theorem from function spaces to dependent products and sums and universes. The key to the proof is the introduction of a suitable notion of density and associated with it a notion of co-density for dependent domains with totality. We show that the universe obtained by closing a given family of basic domains with totality under some quantifiers has a dense and co-dense totality provided the totalities on the basic domains are dense and co-dense and the quantifiers preserve density and co-density. In particular we can show that the quantifiers Π and Σ have this preservation property and hence, for example, the closure of the integers and the booleans (which are dense and co-dense) under Π and Σ has a dense and co-dense totality. We also discuss extensions of the density theorem to iterated universes, i.e. universes closed under universe operators.