The Groupoid-Syntax of Type Theory is a Set

TL;DR

Facing limitations of set-truncated intrinsic syntax in HoTT, the paper introduces GCwF, lifting truncation to groupoids with minimal coherence to permit interpretations in univalent models. It proves that the initial GCwF with $\Pi$-types and a base family is set-truncated, enabling the use of standard intrinsic syntax while connecting to univalent semantics via a set interpretation. A key methodological advance is α-normalisation, showing Ty_G forms a set by constructing $\mathsf{NTy}$ and a retraction, then relating groupoid-syntax to the set-based syntax. Together, these results provide a principled, implementable pathway for interpreting type-theoretic syntax in richer, univalent models and point toward future work on universes and higher coherence.

Abstract

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.

Figures (6)

• Figure 1: This diagram is the proof $\ulcorner\urcorner[\circ]\,(\mathcolor{BrickRed}{\mathsf{El}}\,\hat{A})\,\gamma\,\delta$, which is the outer square. Double lines mean definitional equality. The boundaries of the outer square are definitionally equal to the boundaries of the inner square, which we fill by $\mathsf{El}[\circ]\,\hat{A}\,\gamma\,\delta$.
• Figure 2: This diagram is the proof $\ulcorner\urcorner[\circ]\,(\mathcolor{BrickRed}{\Pi}\,A\,B)\,\gamma\,\delta$. In the upper part, we compute the square to be filled: the left hand side square is definitionally equal to the right hand side one. Then, we fill the right hand side square in the lower diagram, where the boundary of the square is the same as the upper right hand side square.
• Figure 3: This diagram is the proof $\ulcorner\urcorner[\mathsf{id}]\,(\mathcolor{BrickRed}{\Pi}\,A\,B)$. In the upper part, we compute the triangle to be filled: the left hand side triangle is definitionally equal to the right hand side one. Then, we fill the right hand side triangle in the lower diagram, where we duplicate the vertex $\Pi\,\ulcorner\mathcolor{BrickRed}{A}\urcorner\,\ulcorner\mathcolor{BrickRed}{B}\urcorner$ for readability.
• Figure 4: Normalisation on the substitution law for $\Pi$ acts as follows: $\mathsf{norm}\,(\Pi[]\,A\,B\,\gamma) :\equiv \mathcolor{BrickRed}{\Pi}\,\mathsf{refl}\,e$ where $e$ is defined in the upper square in this diagram. The upper square is a dependent square over the lower one.
• Figure 5: This diagram is the proof $\mathsf{compl}\,(\Pi[]\,A\,B\,\gamma)$. The line $e$ is defined in Figure \ref{['fig:normpisub']}.

Theorems & Definitions (12)

• Definition 2: Wild syntax https://csl26-cohtt.github.io/TT.Wild.Syntax.html
• Example 3: Using the wild syntax https://csl26-cohtt.github.io/TT.Wild.Examples.html
• Proposition 5: https://csl26-cohtt.github.io/TT.Wild.NotSet.html#%C2%ACisSetTy
• Definition 6: Set-syntax https://csl26-cohtt.github.io/TT.Set.Syntax.html
• Definition 7: Groupoid-syntax https://csl26-cohtt.github.io/TT.Groupoid.Syntax.html
• Definition 11: $\upalpha$-normal forms https://csl26-cohtt.github.io/TT.Groupoid.NTy.html#NTy
• Lemma 12: https://csl26-cohtt.github.io/TT.Groupoid.NTy.html#isSetNTy
• Theorem 16: https://csl26-cohtt.github.io/TT.Groupoid.NTy.html#isSetTy
• Remark 1
• Definition 19: Groupoid CwF, GCwF https://csl26-cohtt.github.io/TT.Groupoid.CwF.html