Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2509.14988 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917134945222656 |
|---|---|
| author | Altenkirch, Thorsten Kaposi, Ambrus Xie, Szumi |
| author_facet | Altenkirch, Thorsten Kaposi, Ambrus Xie, Szumi |
| contents | Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category.
We demonstrate that the initial GCwF for a type theory with a base family of sets and Pi-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_14988 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Groupoid-Syntax of Type Theory is a Set Altenkirch, Thorsten Kaposi, Ambrus Xie, Szumi Logic in Computer Science Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category. We demonstrate that the initial GCwF for a type theory with a base family of sets and Pi-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda. |
| title | The Groupoid-Syntax of Type Theory is a Set |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.14988 |