Polynat in PER models (Q1434360)

So-called PERs, partial equivalence relations (symmetric and transitive) applied on a partial combinatory algebra (combinators K and S with the standard but partial combinatorial interpretations), form a model for polymorphically typed lambda-calculus (system F). The polymorphic natural number type N (polynat) is used to uniquely represent numbers by (polymorphic) Church numerals. It is shown that the type N is not always polymorphically standard in the PER-model, meaning that the interpretation of the type N contains not only interpretations of the Church numerals. An explicit counterexample is constructed. The paper is well written but too short and too technical to be self-contained. It requires from the reader much deeper introductory study of the subject.