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.