A Model of Type Theory in Groupoid Assemblies

TL;DR

This paper constructs a model of type theory within the category of groupoids internal to assemblies on a partial combinatory algebra, demonstrating advanced categorical and type-theoretic structures.

Contribution

It introduces a $ ext{π}$-tribe structure on groupoid assemblies, shows the existence of W-types with reductions, and establishes a connection to the realizability topos.

Findings

Grpd(Asm$(A)$) forms a $ ext{π}$-tribe, modeling type theory.

The category has W-types with reductions and an impredicative object classifier.

The subcategory pGrpd(Asm$(A)$) has finite bilimits, bicolimits, and its homotopy category is RT$[A]$.

Abstract

We consider the category Grpd(Asm$(A)$) of groupoids defined internally to the category of assemblies on a partial combinatory algebra $A$. In this thesis we exhibit the structure of a $\pi$-tribe on Grpd(Asm$(A)$) showing the category to be a model of type theory. We also show that Grpd(Asm$(A)$) has $W$-types with reductions and univalent object classifier for assemblies and modest assemblies, where the latter is an impredicative object classifier. Using the $W$-types with reductions, we show that Grpd(Asm$(A)$) has a model structure. Finally, we construct pGrpd(Asm$(A)$), the full subcategory of partitioned groupoid assemblies, and show that pGrpd(Asm$(A)$) has finite bilimits and bicolimits as well as showing that the homotopy category of the full subcategory of the $0$-types of pGrpd(Asm$(A)$) is RT$[A]$, the realizability topos of $A$.