Games and definability for system F

We develop a game-theoretic model of the polymorphic λ-calculus, system F, as a fibred category F. Our main result is that every morphism σ of the model defines a normal form s_σ of system F, whose interpretation is σ. Thus the model gives a precise, non-syntactic account of the calculus