# Where is relational parametricity in hyperdoctrine or topos models explored?

Reynolds originally proposed a relational semantics for the second order polymorphic lambda calculus[1]. However he later showed[2] that this approach was inconsistent with classical set theory. Pitts described the framework of hyperdoctrine models and topos models[3] which are consistent with constructive logic.

Presumably relational hyperdoctrine and topos models were then developed. Where can I read about them?

• [1] Types, abstraction and parametric polymorphism
• [2] Polymorphism is not set-theoretic
• [3] Polymorphism is set theoretic, constructively

1. The fact that a (non-parametric) universe of sets interpreting System F means that you can give a parametric model of System F in the internal logic of the topos, much more easily than you can in ordinary set theory. Essentially, you don't have to muck around with PERs, since you can just assume that you have a suitable collection of sets. Bob Atkey used this idea in his paper Relational Parametricity for Higher Kinds, where he worked out parametricity for $F_\omega$ by working in the impredicative calculus of constructions.