Groupoidal Realizability for Intensional Type Theory

TL;DR

This paper develops a homotopical realizability model of intensional type theory using groupoids, where realizers encode non-trivial homotopical information, advancing the understanding of the homotopical BHK interpretation.

Contribution

It introduces partitioned groupoidal assemblies parameterized by realizer categories with an internal interval, modeling intensional type theory with homotopical structure.

Findings

Models intensional 1-truncated type theory without function extensionality.

Establishes an impredicative universe of 1-types in the untyped realizer category.

Provides a groupoidal analogue of traditional realizability models.

Abstract

We develop realizability models of intensional type theory, based on groupoids, wherein realizers themselves carry non-trivial (non-discrete) homotopical structure. In the spirit of realizability, this is intended to formalize a homotopical BHK interpretation, whereby evidence for an identification is a path. Specifically, we study partitioned groupoidal assemblies. Categories of such are parameterised by "realizer categories" (instead of the usual partial combinatory algebras) that come equipped with an interval qua internal cogroupoid. The interval furnishes a notion of homotopy as well as a fundamental groupoid construction. Objects in a base groupoid are realized by points in the fundamental groupoid of some object from the realizer category; isomorphisms in the base groupoid are realized by paths in said fundamental groupoid. The main result is that, under mild conditions on the realizer category, the ensuing category of partitioned groupoidal assemblies models intensional (1-truncated) type theory without function extensionality. Moreover, when the underlying realizer category is "untyped", there exists an impredicative universe of 1-types (the modest fibrations). This is a groupoidal analogue of the traditional situation.