Game semantics of universes

TL;DR

This paper extends game semantics to include the cumulative hierarchy of universes in Martin-Löf type theory, enabling combinatorial reasoning for universes and addressing key challenges with identity types.

Contribution

It provides the first comprehensive game semantics for all standard types in Martin-Löf type theory, including universes, overcoming previous conflicts with identity types.

Findings

Successfully models universes within game semantics

Addresses and resolves the conflict between identity types and universes

Enables new combinatorial reasoning methods for type theory

Abstract

This work extends the present author's computational game semantics of Martin-L\"{o}f type theory to the cumulative hierarchy of universes. This extension completes game semantics of all standard types of Martin-L\"{o}f type theory for the first time in the 30 years history of modern game semantics. As a result, the powerful combinatorial reasoning of game semantics becomes available for the study of universes and types generated by them. A main challenge in achieving game semantics of universes comes from a conflict between identity types and universes: Naive game semantics of the encoding of an identity type by a universe induces a decision procedure on the equality between functions, a contradiction to a well-known fact in recursion theory. We overcome this problem by novel games for universes that encode games for identity types without deciding the equality.