Combinatorial realizability models of type theory

TL;DR

This paper presents a new realizability-based model for Martin-Löf type theory that is sound and complete for its 1-truncated version, combining syntactic and realizability semantics, and analyzing the associated groupoid.

Contribution

It introduces a novel combinatorial realizability model for type theory that unifies syntactic and semantic perspectives, extending the understanding of groupoid semantics.

Findings

Model is sound and complete for 1-truncated type theory

The associated syntactic groupoid has the same homotopy type as the free groupoid generated by a graph G

The model encompasses Hofmann-Streicher groupoid semantics

Abstract

We introduce a new model construction for Martin-L\"{o}f intensional type theory, which is sound and complete for the 1-truncated version of the theory. The model formally combines the syntactic model with a notion of realizability; it also encompasses the well-known Hofmann- Streicher groupoid semantics. As our main application, we use the model to analyse the syntactic groupoid associated to the type theory generated by a graph G, showing that it has the same homotopy type as the free groupoid generated by G.