Game-theoretic Interpretation of Type Theory Part II: Uniqueness of Identity Proofs and Univalence

TL;DR

This paper develops a game semantics model for intensional type theory that refutes uniqueness of identity proofs and supports univalence, advancing the interpretation of homotopy type theory.

Contribution

It introduces predicative gamoids with a groupoid structure to interpret Id-types and univalence within a game semantics framework, extending prior work.

Findings

Refutes the principle of uniqueness of identity proofs.

Validates the univalence axiom within the model.

Provides a concrete groupoid model for homotopy type theory.

Abstract

In the present paper, based on the previous work (Part I), we present a game semantics for the intensional variant of intuitionistic type theory that refutes the principle of uniqueness of identity proofs and validates the univalence axiom, though we do not interpret non-trivial higher propositional equalities. Specifically, following the historic groupoid interpretation by Hofmann and Streicher, we equip predicative games in Part I with a groupoid structure, which gives rise to the notion of (predicative) gamoids. Roughly, gamoids are "games with (computational) equalities specified", which interpret subtleties in Id-types. We then formulate a category with families of predicative gamoids, equipped with dependent product, dependent sum, and Id-types as well as universes, which forms a concrete instance of the groupoid model. We believe that this work is an important stepping-stone towards a complete interpretation of homotopy type theory.