What type of study is this?

This is a Quantitative Study study.

September 22, 2025Open Access

A Model of Type Theory in Groupoid Assemblies

Key Points

Grpd(Asm$(A)$) shows the structure of a $π$-tribe, establishing it as a model of type theory.
It contains $W$-types with reductions and an impredicative object classifier for assemblies.
The constructed pGrpd(Asm$(A)$) exhibits finite bilimits and bicolimits for partitioned groupoids.
The homotopy category of the $0$-types of pGrpd(Asm$(A)$) is identified as RT$[A]$, a realizability topos.

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 π-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 RTA, the realizability topos of A.

Read Full Paperexternally

Bookmark

View Full Paper

Cite This Study

Anthony Agwu (Mon,) studied this question.

synapsesocial.com/papers/68d46fdc31b076d99fa6a749 https://doi.org/https://doi.org/10.48550/arxiv.2507.16062

Bookmark

View Full Paper