Polymorphism and apartness (Q1182690)

The author gives a new intuitionistic model \({\mathcal C}\) for the second- order polymorphic lambda calculus. \({\mathcal C}\) is a proper subcategory of the category \({\mathcal M}\) of realizability-valued modest sets on which earlier intuitionistic models have been constructed. The present construction has the advantage that it does not require Church's thesis nor computability axioms such as ECTs. Only purely set theoretic constructions such as local choice principles are required.