Polymorphism and apartness.
David Charles McCarty · Notre Dame Journal of Formal Logic · 1991
Using traditional intuitionistic concepts such as apartness and subcountability, we give a relatively simple and direct construction of a natural, set-theoretic model for the second-order polymorphic lambda calculus, a model distinct from that of the modest sets.