Non trivial power types can´t be subtypes of polymorphic types

A new, limitative relation between the polymorphic lambda calculus and the kind of higher-order type theory embodied in the logic of topoi is established. It is shown that any embedding in a topos of the Cartesian closed category of (closed) types of a model of the polymorphic lambda calculus must place the polymorphic types well away from the power types σ→Ω of the topos, in the sense that σ→Ω is a subtype of a polymorphic type only in the case that σ is empty (and hence σ→Ω is terminal). As corollaries, strengthening of the Reynolds result on the nonexistence of set-theoretic models of polymorphism are obtained