Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2507.16062 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911070456643584 |
|---|---|
| author | Agwu, Anthony |
| author_facet | Agwu, Anthony |
| contents | 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 RT$[A]$, the realizability topos of $A$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_16062 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Model of Type Theory in Groupoid Assemblies Agwu, Anthony Category Theory 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 RT$[A]$, the realizability topos of $A$. |
| title | A Model of Type Theory in Groupoid Assemblies |
| topic | Category Theory |
| url | https://arxiv.org/abs/2507.16062 |