In standard realizability one works with respect to an untyped universe of realizers called a partial combinatory algebra (pca). It is well known that a pca A gives rise to a categorical model of impredicative type theory via the category Asm(A) of assemblies over A or the realizability topos over A. Recently, John Longley introduced a typed version of pca's (Longley 1999b). The above mentioned construction of categorical models extends to the typed case. However, in general these are no longer impredicative. We show that for a typed pca A the ensuing models are impredicative if and only if A has a universal type U. Such a type U can be endowed with the structure of an untyped pca such that U and A induce equivalent realizability models: in other words, a typed pca A with a universal type is essentially untyped. Thus, a posteriori it turns out that nothing is lost by restricting to (untyped) pca's as far as realizability models of impredicative type theories are concerned. For instance, we show that for a typed pca A the fibred category of discrete families in Asm(A) is small if and only if A has a universal type. As the category of --separated objects of the modified realizability topos is equivalent to Asm(A) for an appropriate type pca A without a universal type, it follows that the discrete families in the subcategory of --separated objects of the modified realizability topos do not provide a model of polymorphic λ-calculus.
展开▼
