Game-theoretic Interpretation of Type Theory Part I: Intuitionistic Type Theory with Universes
Norihiro Yamada · arXiv (Cornell University) · 2016
We present a game semantics for intuitionistic type theory. Concretely, we propose categories with families of games and strategies for both extensional and intensional type theories, which support dependent product, dependent sum, and Id-types as well as universes. The intensional interpretation of the Id-types in particular has interesting phenomena: It admits the principle of uniqueness of identity proofs as well as Streicher's first and second Criteria of Intensionality, but refutes the third criterion, the principles of equality reflection and function extensionality, and the univalence axiom.