Game-theoretic Investigation of Intensional Equalities

TL;DR

This paper introduces a novel game semantics for Martin-Löf type theory that models intensional equalities, refutes UIP, and supports univalence, providing a foundation for interpreting higher equalities in homotopy type theory.

Contribution

It presents the first game semantics for MLTT that refutes UIP and validates univalence, connecting game semantics with homotopy type theory.

Findings

Refutes the principle of uniqueness of identity proofs (UIP).

Validates the univalence axiom (UA).

Provides a categorical model as a substructure of the groupoid model.

Abstract

This article presents a new game semantics for Martin-L\"of type theory (MLTT), in which each game is equipped with selected isomorphism strategies that represent (computational) proofs for (intensional) equality between strategies on the game. These isomorphism strategies interpret propositional equalities in MLTT. As a main result, we have obtained a first game semantics for MLTT that refutes the principle of uniqueness of identity proofs (UIP) and validates univalence axiom (UA) though it does not model non-trivial higher equalities. Categorically, our model forms a substructure of the classic groupoid model of MLTT by Hofmann and Streicher. Similarly to the path from the groupoid model to the $\omega$-groupoid model, we are planning to generalize the game semantics to give rise to an omega-groupoid structure to interpret non-trivial higher equalities in homotopy type theory (HoTT).