# 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.