having issue with numbers in Polymorphic Lambda Calculus
The syntax you written is probably of the System F&lt;:.

However, the typed Church numerals you written are introduced in the context of System F (a.k.a. λ2) at Fig. 11 of the source pdf.

The terms of System F are defined like below in Types and programming languages (Benjamin C. Pierce, MIT press, 2002):

t ::=           terms:
      x         variable
      λx:T.t    abstraction
      t t       application
      λX.t      type abstraction
      t [T]     type application


The typed Church numerals at Fig. 11 are terms in this definition.

Moreover, in System F&lt;:, Church numerals are also well-typed and can be more generalized. Below examples are taken from Types and programming languages. Top is the maximum type.

szero = λX&lt;:Top. λS&lt;:X. λZ&lt;:X. λs:X→S. λz:Z. z;
sone  = λX&lt;:Top. λS&lt;:X. λZ&lt;:X. λs:X→S. λz:Z. s z;