Polymorphism is Set Theoretic, Constructively

We consider models in toposes of equational theories over the type system consisting of the Girard-Reynolds polymorphic lambda calculus augmented with finite product types. The particular notion of model we use is very straightforward, with polymorphic product types and function types both being interpreted in a standard way in the topos - the first by internal products and the second by exponentiation. We show that every hyperdoctrine model of a polymorphic lambda theory can be fully embedded in such a topos model, the topos constructed being simply a functor category. There are precise correspondences between polymorphic lambda theories and their hyperdoctrine models, and between toposes and theories in higher order intuitionistic predicate logic. So we can conclude that every theory of the first kind can be interpreted in a theory of the second kind in such a way that the polymorphic types are interpreted in a standard way, but so that up to provability in the higher order theory, they have exactly the same closed terms as before. A simple corollary of this full embedding result is the completeness of topos models: for each polymorphic lambda theory there is a topos model whose valid equations are exactly those derivable in the theory.