Games and Definability For FPC
Guy McCusker · Bulletin of Symbolic Logic · 1997
Abstract A new games model of the languageFPC, a type theory with products, sums, function spaces and recursive types, is described. A definability result is proved, showing that every finite element of the model is the interpretation of some term of the language.