The Groupoid-Syntax of Type Theory Is a Set

Altenkirch, Thorsten; Kaposi, Ambrus; Xie, Szumi

doi:10.4230/LIPIcs.CSL.2026.40

The Groupoid-Syntax of Type Theory Is a Set

Thorsten Altenkirch

University of Nottingham, UK Ambrus Kaposi

Eötvös Loránd University (ELTE), Budapest, Hungary Szumi Xie

Eötvös Loránd University (ELTE), Budapest, Hungary

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.

Keywords and phrases:

Categorical models of type theory, category with families, groupoids, coherence, homotopy type theory

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Type theory

Supplementary Material:

Software (Source Code): https://bitbucket.org/akaposi/cohtt
archived at

swh:1:dir:13849af00ff393300c0ae6cdd47ba6ddfa0d1cd8

Acknowledgements:

We thank the reviewers for their helpful comments and suggestions. We thank Niels van der Weide for explaining us the relationship to comprehension categories.

Funding:

The first author was supported by project no. TKP2021-NVA-29 which has been implemented with the support provided by the Ministry of Culture and Innovation of Hungary from the National Research, Development and Innovation Fund, financed under the TKP2021-NVA funding scheme. The second and third authors were funded by the European Union (ERC, HOTT, 101170308). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

DOI:

10.4230/LIPIcs.CSL.2026.40

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

In [5], an intrinsically typed syntax for basic type theory using a Quotient-Inductive-Inductive Type (QIIT) was introduced. By intrinsically typed, we mean that the syntax directly enforces typing constraints, eliminating the need for separate untyped preterms needed in extrinsic presentations. The equational theory is integrated naturally using path constructors from Homotopy Type Theory (HoTT), while set-truncation ensures that types behave as sets.

QIITs are a special case of Higher Inductive-Inductive Types (HIITs) where all types are truncated to sets by adding a higher path constructor. The term inductive-inductive signals that constructors can reference other constructors in their types. In essence, [5] defined the syntax of type theory as the initial¹¹1Initiality is equivalent to induction for any QIIT [26], this been generalised to HIITs by Sattler [33]. In this paper, we use the terms initial model and syntax interchangeably. Category with Families (CwF) with $\Pi$ -types and an uninterpreted base family. This allowed the syntax to be interpreted in any CwF with the necessary structure and served as the foundation for a proof of normalisation using Normalisation by Evaluation (NbE) [6].

However, this approach had a significant limitation: the syntax could not be interpreted in the intended model where types are sets. This issue arose due to the use of set truncation, which enforced types to be sets but precluded a univalent semantics, such as $\mathsf{Set}$ . To work around this, inductive-recursive universes were used. While effective, this approach was unsatisfactory as it excluded univalent models, which are natural semantics for type theory.

Simply omitting set truncation is not a solution. Without truncation: (i) we cannot prove necessary equations in the syntax; (ii) the syntax itself is no longer a set, which e.g. makes equality in the syntax undecidable. A fully principled solution would require adding all higher coherences. However, this is both technically complex and generally believed to require a 2-level type theory rather than plain HoTT [29].

In this paper, we propose a middle ground: we lift the truncation level to groupoids and add a minimal set of coherence equations. This enables interpreting the syntax into the set model and other univalent category-based models. This compromise aligns naturally with the structure of categories in HoTT [36], where objects are groupoids with no truncation restriction, while hom-sets remain sets, as their name implies. Actually, if we only restrict types to be groupoids, then we can prove that contexts in the syntax also form a groupoid.

At first glance, this raises a new concern: does lifting to groupoids and adding coherence equations require redefining the syntax? Do we lose decidability of equality? Our main result resolves this concern:

The groupoid-syntax of type theory with $\Pi$ -types and a base family has types and contexts that are sets.

In essence, we retain the set-truncated syntax of type theory while enabling evaluation in groupoid-level models. This allows us to interpret the set-truncated syntax into univalent models, such as $\mathsf{Set}$ or the container model [7]. However, we note that univalence for types cannot be assumed as a principle at the judgmental level – doing so would mean that types are not a set anymore.

Contributions.

The main contributions of this paper are as follows:

$\blacksquare$

We introduce the notion of a Groupoid Category with Families (GCwF) with $\Pi$ -types and a base family (Definition 20).
$\blacksquare$

We show that the initial GCwF with $\Pi$ -types and a base family is set-truncated.
$\blacksquare$

We establish the above proof using an $\upalpha$ -normalisation construction.
$\blacksquare$

As a result, we enable the definition of the univalent set model and other univalent category-based models for the set-truncated syntax.

All results are formalised in Cubical Agda.

Structure of the paper.

After listing related work, we describe our metatheory and notation in Section 2. In Section 3, we define various syntaxes as HIITs and describe the problem of interpreting the set-truncated syntax in sets. In Section 4 we show that the groupoid-syntax is a set. We use this fact in Section 5 to fix the above problem. We conclude in Section 6.

Related work.

This paper is a continuation of the series of papers internalising the intrinsic syntax of type theory in type theory [19, 15] and in homotopy type theory [34, 5]. Intrinsic syntax means that there are only well-formed, well-scoped, well-typed terms which are quotiented by conversion. This is in contrast with extrinsic style formalisations [1, 2]. We use a variant of Dybjer’s CwFs [21] introduced by Ehrhard [22, 17].

Infinite-dimensional versions of our 1-dimensional notion of model are given by Kraus and Uemura. Kraus defines a notion of $\infty$ -CwF [29] inside an extension of type theory with a strict equality (two-level type theory, [3, 9, 10]). He conjectures that the set-level (0-level) syntax is initial for his $\infty$ -model. Uemura [35] proves normalisation for an $\infty$ -dimensional presentation of type theory, however his work is not formalised in intensional type theory.

Our theorem that the initial GCwF with certain type formers is set-truncated can be seen as a simple coherence theorem analogous to that of monoidal categories. Coherence for monoidal categories says that in the free monoidal category over a set of objects, morphisms form a set. Our coherence theorem is for types rather than morphisms (substitutions), and we generate the types from a set-valued family using $\Pi$ and instantiation. Coherence for monoidal groupoids was proven in HoTT by Piceghello [32], where he also used groupoid-truncated HITs to define the free monoidal groupoid.

In HoTT, the ideal solution for coherence problems is to find finite descriptions which imply all the infinitely many coherences. For example, usability of integers defined as set-quotients is limited, but there is a way to define their $\infty$ -version without truncation [8]. Free groups can defined without truncation [30], however originally groupoid-truncation was needed to prove that the free group over a set is a set. The general case was resolved by Wärn [40]. The Symmetry book [11] contains several similar examples.

There are notions of model of type theory weaker than CwFs where e.g. substitution is only functorial up to isomorphism [23, 31, 12]. These are further away from implementations of type theory, but they admit the standard model in the setting of HoTT [37], even without going 2-categorical. 2-categories are used to formulate the equivalence of weaker and stricter notions of model. Dybjer and Clairambault [16] proved the 2-equivalence of locally cartesian closed categories and CwFs with appropriate structure. Van der Weide [37] formalised this result in a univalent setting, for univalent comprehension categories instead of CwFs, and extended it to new type formers.

Higher inductive-inductive types (HIITs) have been used before to describe free algebraic structures such as real numbers [36], the partiality monad [4], or hybrid semantics [20], but all of these are set-truncated HIITs, unlike our groupoid-syntax. Cubical type theory supports HITs [18, 14], and there is a scheme for describing HIITs [25] which covers our usages.

2 Metatheory and formalisation

Everything in this paper is formalised in Cubical Agda [38], the formalisation is available as supplementary material. Next to definitions/theorems/etc., icons point to the corresponding part in the HTML version of the source code. In the paper text, we use informal cubical type theory: this means that we do not refer to the interval and instead of using 3-dimensional cubes, we only compose and fill larger 2-dimensional shapes.

We write $\equiv$ for equations holding definitionally, $:\equiv$ denotes definitions. Dependent function space is written $(x:A)\to B$ or $\forall x\ldotp B$ , we also use implicit quantifications. We write dependent pairs as $(x:A)\times B$ , the empty type as $\bot$ , the unit type as $\top$ . The universe of types is $\mathsf{Type}$ , we also use the universe of h-sets $\mathsf{Set}$ and h-groupoids $\mathsf{Groupoid}$ . We have a predicative universe hierarchy, but we do not write levels for readability. The identity (path, equality) type is written $a=_{A}b$ for $a, b : A$ , where the subscript _A is usually ommitted. The dependent path type (PathP, heterogeneous equality) is written $b_{0}=_{B}^{e}b_{1}$ for $e:a_{0}=a_{1}$ and $b_{i}:B\,a_{i}$ , sometimes the subscript _B is ommitted. We overload functions and their congruence (ap operator), e.g. $f\,e:f\,a=f\,b$ where $e:a=b$ , and we omit symmetries as well. Transport is written $e_{*}\,b_{0}:B\,a_{1}$ for $e:a_{0}=a_{1}$ and $b_{0}:B\,a_{0}$ , we tend to give a separate name for operations using transport (e.g. $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}]^{\mathsf{U}}$ is a transported version of $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}]$ ). The obvious element of the heterogeneous equality $b_{0}=_{B}^{e}\,e_{*}\,b_{0}$ is called $\mathrm{transportFiller}$ . The composition operator of cubical type theory is the generalisation of transitivity as depicted below, it also comes with a filler operation.

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-% page-1.pdf2svg.svg}\end{matrix}

For the composite equality $e$ , we denote the filler by $\mathrm{fillerOf}\,e$ . Some of these composition and filling operations are primitive in cubical type theory, but they are also definable via the eliminator of the identity type (J). In this paper we abstract over these differences.

We write compositions with equational reasoning by $a_{0}\overset{e_{1}}{=}a_{1}\overset{e_{2}}{=}\dots\overset{e_{n}}{=}a_{n}$ , or its multi-line variant (left, below). Composition also works for heterogeneous equalities, in this case we write the base equalities in superscripts (right, below).

$\displaystyle a_{0}$	$\displaystyle{=}(e_{1})$	$\displaystyle b_{0}$	$\displaystyle{=}^{e_{1}}(e^{\prime}_{1})$
$\displaystyle\dots$		$\displaystyle\dots$
$\displaystyle a_{n-1}$	$\displaystyle{=}(e_{n})\hskip 90.00014pt$	$\displaystyle b_{n-1}$	$\displaystyle{=}^{e_{n}}(e^{\prime}_{n})$
$\displaystyle a_{n}$		$\displaystyle b_{n}$

Here $b_{i}:B\,a_{i}$ , $e_{i}:a_{i-1}=a_{i}$ and $e^{\prime}_{i}:b_{i-1}=_{B}^{e_{i}}b_{i}$ , and the resulting heterogeneous equality is $b_{0}=_{B}^{\text{composite of the $e_{i}$s}}b_{n}$ . We denote heterogeneous composition and filling of shapes by drawing a base diagram and a dependent diagram. We say that the right diagram is over the left one: in this case the dotted composition line has type $b_{0}=_{B}^{e_{0}}\,b_{n}$ .

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-% page-2.pdf2svg.svg}\end{matrix}

Some squares can be filled by the fact that every parameterised path is natural. We denote these naturality squares by writing $\mathrm{nat}$ in the center:

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-% page-3.pdf2svg.svg}\end{matrix}

There are some technical limitations of Cubical Agda that we have to circumvent in the formalisation, but are not visible in the text of this paper. We summarise these below.

\blacksquare

Interleaved constructors of (higher) inductive-inductive datatypes are not allowed in Cubical Agda. For example, this fragment of a syntax of a type theory is not allowed:

$\displaystyle\mathsf{Con}$	$\displaystyle:\mathsf{Type}$	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\triangleright\mathord% {\hskip 1.0pt\text{--}\hskip 1.0pt}$	$\displaystyle:(\mathit{\Gamma}:\mathsf{Con})\to\mathsf{Ty}\,\mathit{\Gamma}\to% \mathsf{Con}$
$\displaystyle\mathsf{Ty}$	$\displaystyle:\mathsf{Con}\to\mathsf{Type}\hskip 60.00009pt$	$\displaystyle\Sigma$	$\displaystyle:(A:\mathsf{Ty}\,\mathit{\Gamma})\to\mathsf{Ty}\,(\mathit{\Gamma}% \triangleright A)\to\mathsf{Ty}\,\mathit{\Gamma}$
$\displaystyle\mathsf{eq}$	$\displaystyle:\mathit{\Gamma}\triangleright\Sigma\,A\,B=_{\mathsf{Con}}\mathit% {\Gamma}\triangleright A\triangleright B$

Here every later constructor depends on all the previous constructors, the order cannot be modified, and first we have a $\mathsf{Con}$ -constructor, then a $\mathsf{Ty}$ -constructor, then another $\mathsf{Con}$ -constructor. We solve this via the encoding proposed in [24], which uses the same idea as encoding mutual inductive types as an indexed family [27]: we introduce a sort of codes $\mathsf{Code}$ and a family of elements $\mathsf{EL}$ , and then all constructors are in the same sort:

$\displaystyle\mathsf{Code}$	$\displaystyle:\mathsf{Type}$	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\triangleright\mathord% {\hskip 1.0pt\text{--}\hskip 1.0pt}$	$\displaystyle:(\mathit{\Gamma}:\mathsf{EL}\,\mathsf{Con})\to\mathsf{EL}\,(% \mathsf{Ty}\,\mathit{\Gamma})\to\mathsf{EL}\,\mathsf{Con}$
$\displaystyle\mathsf{EL}$	$\displaystyle:\mathsf{Code}\to\mathsf{Type}$	$\displaystyle\Sigma$	$\displaystyle:(A:\mathsf{EL}\,(\mathsf{Ty}\,\mathit{\Gamma}))\to\mathsf{EL}\,(% \mathsf{Ty}\,(\mathit{\Gamma}\triangleright A))\to\mathsf{EL}\,(\mathsf{Ty}\,% \mathit{\Gamma})$
$\displaystyle\mathsf{Con}$	$\displaystyle:\mathsf{Code}$	$\displaystyle\mathsf{eq}$	$\displaystyle:\mathit{\Gamma}\triangleright\Sigma\,A\,B=_{\mathsf{EL}\,\mathsf% {Con}}\mathit{\Gamma}\triangleright A\triangleright B$
$\displaystyle\mathsf{Ty}$	$\displaystyle:\mathsf{EL}\,\mathsf{Con}\to\mathsf{Code}\hskip 38.99998pt$

We use the same technique when defining our syntaxes (Definitions 2, 6, 7).

$\blacksquare$

When we describe HIITs, we use transport and composition, but in the formalisation, we avoid them (we still use composition operators in some 2-paths). The reason is twofold: (i) Agda does not see that these operations preserve strict positivity; (ii) as the $\upbeta$ rule for transport is not definitional, it makes it difficult to formalise strict models such as the $\mathsf{Type}$ -interpretation. Instead, we make sure that all transports appear outermost and then can be encoded via dependent paths (a dependent path on $\mathsf{refl}$ computes to a nondependent one). When it is not possible to do this, we add extra constructors together with equations which singleton contract them. For example, in the text of the paper we write the substitution law for $\mathsf{El}$ using a transport: $(\mathsf{El}\,\hat{A})[\gamma]=\mathsf{El}\,\big((\mathsf{U}[]\,\gamma)_{*}\,(% \hat{A}[\gamma])\big)$ . In the formalisation, we introduce a new constructor $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}]^{\mathsf{U}}:\mathsf{Tm}\,\mathit{\Gamma}\,\mathsf{U}\to\mathsf% {Sub}\,\mathit{\Delta}\,\mathit{\Gamma}\to\mathsf{Tm}\,\mathit{\Delta}\,% \mathsf{U}$ together with the contracting equation $\hat{A}[\gamma]=^{\mathsf{U}[]\,\gamma}\hat{A}[\gamma]^{\mathsf{U}}$ , and then use this new constructor when describing $\mathsf{El}[]$ .
$\blacksquare$

When characterising the equality of normal types, in the formalisation we use the inductively defined Martin-Löf identity type instead of the built-in path type (note that they are equivalent). This is convenient because J computes definitionally on its constructor $\mathsf{refl}$ . In the text of the paper we abstract over this.

3 Variants of the syntax and the set interpretation

In this section we define three different variants of the syntax of a type theory with dependent function space and a base family: the wild syntax, the set-truncated and the groupoid-truncated syntax. We show that types in the wild syntax do not form a set, so in particular they cannot have decidable equality. The set-syntax cannot be interpreted into the set model directly, while the groupoid-syntax can.

Parameter 1.

Everything in this section is parameterised by an $X:\mathsf{Set}$ and a $Y:X\to\mathsf{Set}$ .

Definition 2 (Wild syntax ).

We define a higher inductive-inductive type with four sorts. It starts with a category with a terminal object. Objects are called contexts and morphisms are called substitutions, the terminal object is called the empty context. Note that composition $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}$ takes the $\mathit{\Gamma}$ , $\mathit{\Delta}$ and $\mathit{\Theta}$ arguments implicitly, and similarly for all the forthcoming operations and equations.

$\displaystyle\mathsf{Con}$	$\displaystyle:\mathsf{Type}$	$\displaystyle\mathsf{idl}$	$\displaystyle:\forall\gamma\ldotp\mathsf{id}\circ\gamma=\gamma$
$\displaystyle\mathsf{Sub}$	$\displaystyle:\mathsf{Con}\to\mathsf{Con}\to\mathsf{Type}$	$\displaystyle\mathsf{idr}$	$\displaystyle:\forall\gamma\ldotp\gamma\circ\mathsf{id}=\gamma$
$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ\mathord{\hskip 1% .0pt\text{--}\hskip 1.0pt}$	$\displaystyle:\mathsf{Sub}\,\mathit{\Delta}\,\mathit{\Gamma}\to\mathsf{Sub}\,% \mathit{\Theta}\,\mathit{\Delta}\to\mathsf{Sub}\,\mathit{\Theta}\,\mathit{% \Gamma}\hskip 50.00008pt$	$\displaystyle{\diamond}$	$\displaystyle:\mathsf{Con}$
$\displaystyle\mathsf{ass}$	$\displaystyle:\forall\gamma\,\delta\,\theta\ldotp\gamma\circ(\delta\circ\theta% )=(\gamma\circ\delta)\circ\theta$	$\displaystyle\upvarepsilon$	$\displaystyle:\mathsf{Sub}\,\mathit{\Gamma}\,\diamond$
$\displaystyle\mathsf{id}$	$\displaystyle:\mathsf{Sub}\,\mathit{\Gamma}\,\mathit{\Gamma}$	$\displaystyle{\diamond}\upeta$	$\displaystyle:(\sigma:\mathsf{Sub}\,\mathit{\Gamma}\,{\diamond})\to\sigma=\upvarepsilon$

Types form a presheaf over the category of contexts and substitutions. The action on morphisms is called instantiation, it uses a flipped notation because of contravariance.

	$\displaystyle\mathsf{Ty}$	$\displaystyle:\mathsf{Con}\to\mathsf{Type}$	$\displaystyle[{\circ}]$	$\displaystyle:\forall A\,\gamma\,\delta\ldotp A[\gamma\circ\delta]=A[\gamma][\delta]$
	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}]$	$\displaystyle:\mathsf{Ty}\,\mathit{\Gamma}\to\mathsf{Sub}\,\mathit{\Delta}\,% \mathit{\Gamma}\to\mathsf{Ty}\,\mathit{\Delta}\hskip 84.00006pt$	$\displaystyle[\mathsf{id}]$	$\displaystyle:\forall A\ldotp A[\mathsf{id}]=A$

Terms form a dependent presheaf over types. The instantiation operation is overloaded. Note that the functor laws are paths dependent over the functor laws for $\mathsf{Ty}$ .

	$\displaystyle\mathsf{Tm}$	$\displaystyle:(\mathit{\Gamma}:\mathsf{Con})\to\mathsf{Ty}\,\mathit{\Gamma}\to% \mathsf{Type}$	$\displaystyle[{\circ}]$	$\displaystyle:\forall a\,\gamma\,\delta\ldotp a[\gamma\circ\delta]=_{\mathsf{% Tm}\,\mathit{\Theta}}^{[{\circ}]\,A\,\gamma\,\delta}a[\gamma][\delta]$
	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}]$	$\displaystyle:\mathsf{Tm}\,\mathit{\Gamma}\,A\to(\gamma:\mathsf{Sub}\,\mathit{% \Delta}\,\mathit{\Gamma})\to\mathsf{Tm}\,\mathit{\Delta}\,(A[\gamma])\hskip 16% .00008pt$	$\displaystyle[\mathsf{id}]$	$\displaystyle:\forall a\ldotp a[\mathsf{id}]=_{\mathsf{Tm}\,\mathit{\Gamma}}^{% [\mathsf{id}]\,A}a$

In addition to context extension (infix triangle), we have lifting of substitutions which is its functorial action on morphisms. The functor laws again depend on those for $\mathsf{Ty}$ .

	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\triangleright\mathord% {\hskip 1.0pt\text{--}\hskip 1.0pt}$	$\displaystyle:(\mathit{\Gamma}:\mathsf{Con})\to\mathsf{Ty}\,\mathit{\Gamma}\to% \mathsf{Con}$	$\displaystyle{\circ}^{+}$	$\displaystyle:\forall\gamma\,\delta\,\ldotp(\gamma\circ\delta)^{+}=^{[{\circ}]% \,A\,\gamma\,\delta}\gamma^{+}\circ\delta^{+}$
	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{+}$	$\displaystyle:(\gamma:\mathsf{Sub}\,\mathit{\Delta}\,\mathit{\Gamma})\to% \mathsf{Sub}\,(\mathit{\Delta}\triangleright A[\gamma])\,(\mathit{\Gamma}% \triangleright A)\hskip 18.99995pt$	$\displaystyle\mathsf{id}^{+}$	$\displaystyle:\mathsf{id}^{+}=^{[\mathsf{id}]\,A}\mathsf{id}$

We have weakening $\mathsf{p}$ (or first projection), and zero De Bruijn index $\mathsf{q}$ (second projection). We explain how to compose either with lifted substitutions.

\displaystyle\mathsf{p}

\displaystyle:\mathsf{Sub}\,(\mathit{\Gamma}\triangleright A)\,\mathit{\Gamma}% \hskip 12.50002pt

\displaystyle\mathsf{q}

\displaystyle:\mathsf{Tm}\,(\mathit{\Gamma}\triangleright A)\,(A[\mathsf{p}])% \hskip 12.50002pt

\displaystyle\mathsf{p}{\circ}^{+}

\displaystyle:\forall\gamma\ldotp\mathsf{p}\circ\gamma^{+}=\gamma\circ\mathsf{% p}\hskip 12.50002pt

\displaystyle\mathsf{q}[^{+}]

\displaystyle:\forall\gamma\ldotp\mathsf{q}[\gamma^{+}]=^{e}\mathsf{q}

The last equation is heterogeneous over the previous one, $e$ abbreviates the following composite path in $\mathsf{Ty}\,(\mathit{\Delta}\triangleright A[\gamma])$ : $A[\mathsf{p}][\gamma^{+}]\overset{[{\circ}]\,A\,\mathsf{p}\,\gamma^{+}}{=}A[% \mathsf{p}\circ\gamma^{+}]\overset{\mathsf{p}{\circ}^{+}\,\gamma}{=}A[\gamma% \circ\mathsf{p}]\overset{[{\circ}]\,A\,\gamma\,\mathsf{p}}{=}A[\gamma][\mathsf% {p}].$

So far we have all weakenings and variables, for example De Bruijn index $3$ is given by $\mathsf{q}[\mathsf{p}][\mathsf{p}][\mathsf{p}]$ . Now we introduce single substitutions via $\langle a\rangle$ which instantiates the last variable in the context by $a$ , and leaves the rest. It commutes with any substitution, and we explain how to compose $\mathsf{p}$ and $\mathsf{q}$ with single substitutions.

	$\displaystyle\langle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rangle$	$\displaystyle:\mathsf{Tm}\,\mathit{\Gamma}\,A\to\mathsf{Sub}\,\mathit{\Gamma}% \,(\mathit{\Gamma}\triangleright A)$	$\displaystyle\mathsf{p}{\circ}\langle\rangle$	$\displaystyle:\forall a\ldotp\mathsf{p}\circ\langle a\rangle=\mathsf{id}$
	$\displaystyle\langle\rangle{\circ}$	$\displaystyle:\forall a\,\gamma\ldotp\langle a\rangle\circ\gamma=\gamma^{+}% \circ\langle a[\gamma]\rangle\hskip 60.00009pt$	$\displaystyle\mathsf{q}[\langle\rangle]$	$\displaystyle:\forall a\ldotp\mathsf{q}[\langle a\rangle]=^{e}a$

Again, the last equation is heterogeneous over the previous one, where $e$ abbreviates the following path in $\mathsf{Ty}\,\mathit{\Gamma}$ : $A[\mathsf{p}][\langle a\rangle]\overset{[{\circ}]\,A\,\mathsf{p}\,\langle a% \rangle}{=}A[\mathsf{p}\circ\langle a\rangle]\overset{\mathsf{p}{\circ}\langle% \rangle}{=}A[\mathsf{id}]\overset{[\mathsf{id}]\,A}{=}A.$

The last equation for the substitution calculus is an $\upeta$ law explaining that an identity substitution on an extended context is given by $\mathsf{p}$ and $\mathsf{q}$ .

\displaystyle{\triangleright}\upeta

\displaystyle:\mathsf{id}=\mathsf{p}^{+}\circ\langle\mathsf{q}\rangle

We have a base type and a family over it, and elements of these coming from the parameters.

\displaystyle\mathsf{U}

\displaystyle:\mathsf{Ty}\,\mathit{\Gamma}\hskip 18.99995pt

\displaystyle\mathsf{El}

\displaystyle:\mathsf{Tm}\,\mathit{\Gamma}\,\mathsf{U}\to\mathsf{Ty}\,\mathit{% \Gamma}\hskip 18.99995pt

\displaystyle\mathsf{inU}

\displaystyle:X\to\mathsf{Tm}\,\diamond\,\mathsf{U}\hskip 18.99995pt

\displaystyle\mathsf{inEl}

\displaystyle:Y\,x\to\mathsf{Tm}\,\diamond\,(\mathsf{El}\,(\mathsf{inU}\,x))

The substitution law for $\mathsf{U}$ is easy. To express $\mathsf{El}[]$ , we introduce notation for the instantiation operation of terms of type $\mathsf{U}$ , which is just a transported version of ordinary instantiation.

	$\displaystyle\mathsf{U}[]$	$\displaystyle:\forall\gamma\ldotp\mathsf{U}[\gamma]=\mathsf{U}$	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}]^{\mathsf{U}}$	$\displaystyle:\mathsf{Tm}\,\mathit{\Gamma}\,\mathsf{U}\to\mathsf{Sub}\,\mathit% {\Delta}\,\mathit{\Gamma}\to\mathsf{Tm}\,\mathit{\Delta}\,\mathsf{U}$
	$\displaystyle\mathsf{El}[]$	$\displaystyle:\forall\gamma\ldotp(\mathsf{El}\,\hat{A})[\gamma]=\mathsf{El}\,(% \hat{A}[\gamma]^{\mathsf{U}})\hskip 70.0001pt$	$\displaystyle\hat{A}[\gamma]^{\mathsf{U}}$	$\displaystyle:\equiv(\mathsf{U}[]\,\gamma)_{*}\,\hat{A}[\gamma]$

We introduce a transport-filler heterogeneous equality for each $\hat{A}$ and $\gamma$ that we will make use of later: $\hat{A}[\gamma]^{\mathsf{U}}\mathsf{filler}:\hat{A}[\gamma]=^{\mathsf{U}[]\,% \gamma}\hat{A}[\gamma]^{\mathsf{U}}.$

Dependent function space with $\upbeta$ , $\upeta$ laws is defined by the isomorphism $\mathsf{Tm}\,(\mathit{\Gamma}\triangleright A)\,B\cong\mathsf{Tm}\,\mathit{% \Gamma}\,(\Pi\,A\,B)$ natural in $\mathit{\Gamma}$ . It is enough to state naturality in one direction.

$\displaystyle\Pi$	$\displaystyle:(A:\mathsf{Ty}\,\mathit{\Gamma})\to\mathsf{Ty}\,(\mathit{\Gamma}% \triangleright A)\to\mathsf{Ty}\,\mathit{\Gamma}$	$\displaystyle\Pi\upbeta$	$\displaystyle:\forall b\ldotp\mathsf{app}\,(\mathsf{lam}\,b)=b$
$\displaystyle\Pi[]$	$\displaystyle:\forall A\,B\,\gamma\ldotp(\Pi\,A\,B)[\gamma]=\Pi\,(A[\gamma])\,% (B[\gamma^{+}])\hskip 11.49995pt$	$\displaystyle\Pi\upeta$	$\displaystyle:\forall f\ldotp\mathsf{lam}\,(\mathsf{app}\,f)=f$
$\displaystyle\mathsf{lam}$	$\displaystyle:\mathsf{Tm}\,(\mathit{\Gamma}\triangleright A)\,B\to\mathsf{Tm}% \,\mathit{\Gamma}\,(\Pi\,A\,B)$	$\displaystyle\mathsf{lam}[]$	$\displaystyle:\forall b\,\gamma\ldotp(\mathsf{lam}\,b)[\gamma]=^{\Pi[]\,A\,B\,% \gamma}\mathsf{lam}\,(b[\gamma^{+}])$
$\displaystyle\mathsf{app}$	$\displaystyle:\mathsf{Tm}\,\mathit{\Gamma}\,(\Pi\,A\,B)\to\mathsf{Tm}\,(% \mathit{\Gamma}\triangleright A)\,B$

This concludes the definition of the wild syntax.

We defined the substitution calculus in Ehrhard’s style [22, 17] instead of the more usual category with families (CwF) [21, 13]. These two presentations of the substitution calculus are isomorphic. In the above syntax, substitution extension $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt},\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}:(\gamma:\mathsf{Sub}\,\mathit{\Delta}\,\mathit{\Gamma})\to% \mathsf{Tm}\,\mathit{\Delta}\,(A[\gamma])\to\mathsf{Sub}\,\mathit{\Delta}\,(% \mathit{\Gamma}\triangleright A)$ is defined as $(\gamma,a):\equiv\gamma^{+}\circ\langle a\rangle$ . In the other direction, $\gamma^{+}:\equiv\big(\gamma\circ\mathsf{p},([{\circ}]\,A\,\gamma\,\mathsf{p})% _{*}\,\mathsf{q}\big)$ and $\langle a\rangle:\equiv(\mathsf{id},([\mathsf{id}]\,A)_{*}\,a)$ .

Although CwFs have one less operation and fewer equations, we chose the Ehrhard style syntax as there is no need to use the transport operation when specifying the equations. In CwFs, the naturality of substitution extension needs a transport in the middle: $(\gamma,a)\circ\delta=\big(\gamma\circ\delta,([{\circ}]\,A\,\gamma\,\delta)_{*% }\,(a[\delta])\big)$ In our syntax, all the transports are outermost, hence can be encoded by dependent paths.

Example 3 (Using the wild syntax ).

We derive the other direction of naturality for the $\Pi$ -isomorphism: this is the substitution law for $\mathsf{app}$ called $\mathsf{app}[]$ .

	$\displaystyle(\mathsf{app}\,t)[\gamma^{+}]$	$\displaystyle{=}(\Pi\upbeta\,t)$
	$\displaystyle\mathsf{app}\,\Big(\mathsf{lam}\,\big((\mathsf{app}\,t)[\gamma^{+% }]\big)\Big)$	$\displaystyle{=}(\mathsf{lam}[]\,(\mathsf{app}\,t)\,\gamma^{+})$
	$\displaystyle\mathsf{app}\,\bigg((\Pi[]\,A\,B\,\gamma)_{*}\,\Big(\big(\mathsf{% lam}\,(\mathsf{app}\,t)\big)[\gamma]\Big)\bigg)\;$	$\displaystyle{=}(\Pi\upeta\,t)$
	$\displaystyle\mathsf{app}\,\big((\Pi[]\,A\,B\,\gamma)_{*}\,(t[\gamma])\big)$

Nondependent function space is encoded as $A\Rightarrow B:\equiv\Pi\,A\,(B[\mathsf{p}])$ .

The identity function for the family $\mathsf{U}$ , $\mathsf{El}$ is defined as

\displaystyle\mathsf{ID}:\mathsf{Tm}\,\diamond\,(\Pi\,\mathsf{U}\,(\mathsf{El}% \,((\mathsf{U}[]\,\mathsf{p})_{*}\,\mathsf{q})\Rightarrow\mathsf{El}\,((% \mathsf{U}[]\,\mathsf{p})_{*}\,\mathsf{q})))\hskip 56.00014pt

\displaystyle\mathsf{ID}:\equiv\mathsf{lam}\,(\mathsf{lam}\,\mathsf{q})

Note that we had to transport the zero De Bruijn index $\mathsf{q}:\mathsf{Tm}\,(\diamond\triangleright\mathsf{U})\,(\mathsf{U}[% \mathsf{p}])$ so that we can apply $\mathsf{El}$ to it: $(\mathsf{U}[]\,\mathsf{p})_{*}\,\mathsf{q}:\mathsf{Tm}\,(\diamond% \triangleright\mathsf{U})\,\mathsf{U}$ .

In the syntax, we have the categorical application operation for $\Pi$ . Ordinary application is given by $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\cdot\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}:\mathsf{Tm}\,\mathit{\Gamma}\,(\Pi\,A\,B)\to(a:\mathsf{Tm}\,% \mathit{\Gamma}\,A)\to\mathsf{Tm}\,\mathit{\Gamma}\,(B[\langle a\rangle])$ defined as $t\cdot a:\equiv(\mathsf{app}\,t)[\langle a\rangle]$ . It is easy to prove its $\upbeta$ law $(\mathsf{lam}\,t)\cdot a\equiv\mathsf{app}\,(\mathsf{lam}\,t)[\langle a\rangle% ]\overset{\Pi\upbeta\,t}{=}t[\langle a\rangle],$ but the $\upeta$ law is more involved as it needs several transports. We prove it via heterogeneous equality reasoning, where the proof of the equality of the types is written in the superscript of the equality sign.

	$\displaystyle f$	$\displaystyle{=}(\Pi\upeta\,f)$
	$\displaystyle\mathsf{lam}\,(\mathsf{app}\,f)$	$\displaystyle{=^{[\mathsf{id}]\,B}}([\mathsf{id}]\,(\mathsf{app}\,f))$
	$\displaystyle\mathsf{lam}\,\big((\mathsf{app}\,f)[\mathsf{id}]\big)$	$\displaystyle{=^{{\triangleright}\upeta}}({\triangleright}\upeta)$
	$\displaystyle\mathsf{lam}\,\big((\mathsf{app}\,f)[\mathsf{p}^{+}\circ\langle% \mathsf{q}\rangle]\big)$	$\displaystyle{=^{[\circ]\,B\,\mathsf{p}^{+}\,\langle\mathsf{q}\rangle}}([{% \circ}]\,(\mathsf{app}\,f)\,\mathsf{p}^{+}\,\langle\mathsf{q}\rangle)$
	$\displaystyle\mathsf{lam}\,\big((\mathsf{app}\,f)[\mathsf{p}^{+}][\langle% \mathsf{q}\rangle]\big)$	$\displaystyle{=}(\mathsf{app}[]\,t\,\mathsf{p})$
	$\displaystyle\mathsf{lam}\,\Big(\mathsf{app}\,\big((\Pi[]\,A\,B\,p)_{*}\,(f[% \mathsf{p}])\big)[\langle\mathsf{q}\rangle]\Big)\,$	$\displaystyle{\equiv}$
	$\displaystyle\mathsf{lam}\,\big((\Pi[]\,A\,B\,p)_{*}\,(f[\mathsf{p}])\cdot% \mathsf{q}\big)\hskip 11.00008pt$

The type of the above heterogeneous equality is $f=^{e}_{\mathsf{Tm}\,\mathit{\Gamma}\,(\Pi\,A\,\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt})}\mathsf{lam}\,\big((\Pi[]\,A\,B\,p)_{*}\,(f[\mathsf{p}])\cdot% \mathsf{q}\big),$ where $e$ is the following composite of the three heterogeneous steps in the above equality reasoning: $B\overset{[\mathsf{id}]\,B}{=}B[\mathsf{id}]\overset{{\triangleright}\upeta}{=% }B[\mathsf{p}^{+}\circ\langle\mathsf{q}\rangle]\overset{[\circ]\,B\,\mathsf{p}% ^{+}\,\langle\mathsf{q}\rangle}{=}B[\mathsf{p}^{+}][\langle\mathsf{q}\rangle].$

Problem 4 (Type interpretation of the wild syntax ).

As a sanity check for our wild syntax, we define its type (standard, metacircular) interpretation.²²2Following Voevodsky [39], we call a proof relevant theorem a problem and its proof a construction.

Construction.

We define the following four recursive-recursive functions by pattern matching on the constructors of the higher inductive-inductive type.

	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Con}\to\mathsf{Type}$	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Ty}\,\mathit{\Gamma}\to\llbracket\mathit{\Gamma}% \rrbracket\to\mathsf{Type}$
	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Sub}\,\mathit{\Delta}\,\mathit{\Gamma}\to\llbracket% \mathit{\Delta}\rrbracket\to\llbracket\mathit{\Gamma}\rrbracket\hskip 60.00009pt$	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Tm}\,\mathit{\Gamma}\,A\to(\gamma:\llbracket\mathit{% \Gamma}\rrbracket)\to\llbracket A\rrbracket\,\gamma$

Composition is function composition ( $\llbracket\gamma\circ\delta\rrbracket\,\bar{\theta}:\equiv\llbracket\gamma% \rrbracket\,(\llbracket\delta\rrbracket\,\bar{\theta})$ ), identity is identity ( $\llbracket\mathsf{id}\rrbracket\,\bar{\gamma}:\equiv\bar{\gamma}$ ), instantiation is composition ( $\llbracket A[\gamma]\rrbracket\,\bar{\delta}:\equiv\llbracket A\rrbracket\,(% \llbracket\gamma\rrbracket\,\bar{\delta})$ ), context extension is dependent sum ( $\llbracket\mathit{\Gamma}\triangleright A\rrbracket:\equiv(\bar{\gamma}:% \llbracket\mathit{\Gamma}\rrbracket)\times\llbracket A\rrbracket\,\bar{\gamma}$ ), lifting is $\llbracket\gamma^{+}\rrbracket\,(\bar{\delta},\bar{a}):\equiv(\llbracket\gamma% \rrbracket\,\bar{\delta},\bar{a})$ , $\mathsf{p}$ and $\mathsf{q}$ are first and second projections, single substitution is $\llbracket\langle a\rangle\rrbracket\,\bar{\gamma}:\equiv(\bar{\gamma},% \llbracket a\rrbracket\,\bar{\gamma})$ . Function space is interpreted by metatheoretic functions ( $\llbracket\Pi\,A\,B\rrbracket\,\bar{\gamma}:\equiv(\bar{a}:\llbracket A% \rrbracket)\to\llbracket B\rrbracket\,(\bar{\gamma},\bar{a})$ ). $\mathsf{U}$ and $\mathsf{El}$ are interpreted by $X$ and $Y$ , $\mathsf{inU}$ and $\mathsf{inEl}$ simply return their arguments. All the equations are $\mathsf{refl}$ . $\hfill\blacktriangleleft$ The standard interpretation shows that our theory is consistent, that is, not all types are inhabited: $\mathsf{Tm}\,\diamond\,\mathsf{U}$ is interpreted by $\top\to X$ so it is inhabited if and only if $X$ is.

Proposition 5 ().

Types in the wild syntax ( $\mathsf{Ty}\,\mathit{\Gamma}$ for a $\mathit{\Gamma}:\mathsf{Con}$ ) do not form a set.

Proof.

Every higher inductive type, including our Definition 2 can be interpreted into the unit type where all paths are interpreted by $\mathsf{refl}$ . We use a variant of this where every sort is interpreted by $\top$ except $\mathsf{Ty}\,\mathit{\Gamma}$ is interpreted by the circle $\mathsf{S}^{1}$ . $\Pi$ , $\mathsf{U}$ and $\mathsf{El}$ are constant $\mathsf{base}$ , $A[\gamma]$ is interpreted by the interpretation of $A$ . All equations are interpreted by $\mathsf{refl}$ , except $\mathsf{U}[]$ which is interpreted by $\mathsf{loop}$ . The two different proofs of $\mathsf{U}[\mathsf{id}]=\mathsf{U}$ , namely $[\mathsf{id}]\,\mathsf{U}$ and $\mathsf{U}[]\,\mathsf{id}$ are interpreted by $\mathsf{refl}$ and $\mathsf{loop}$ , respectively. $\hfill\blacktriangleleft$ When using the wild syntax, this is a practical problem: it can happen that we need a term of type $\mathsf{El}\,((\mathsf{U}[]\,\mathsf{id})_{*}\,a)$ , but we only have a term of type $\mathsf{El}\,(([\mathsf{id}]\,\mathsf{U})_{*}\,a)$ available. From a broader perspective, Hedberg’s theorem [36, Theorem 7.2.5] implies that we cannot prove normalisation for the wild syntax. In principle, there could be a clever way of defining the equations in the syntax such that there is only one proof for each equation. It is not known whether this is possible [34]. Instead, we make all the equations equal by force.

Definition 6 (Set-syntax ).

The set-based syntax is the wild syntax (Definition 2) extended with the following three higher equality constructors. They truncate substitutions, types and terms to sets.

	$\displaystyle\mathsf{isSetTy}$	$\displaystyle:(e\,e^{\prime}:A_{0}=_{\mathsf{Ty}\,\mathit{\Gamma}}A_{1})\to e=% e^{\prime}$
	$\displaystyle\mathsf{isSetSub}$	$\displaystyle:(e\,e^{\prime}:\gamma_{0}=_{\mathsf{Sub}\,\mathit{\Delta}\,% \mathit{\Gamma}}\gamma_{1})\to e=e^{\prime}\hskip 30.00005pt$	$\displaystyle\mathsf{isSetTm}$	$\displaystyle:(e\,e^{\prime}:a_{0}=_{\mathsf{Tm}\,\mathit{\Gamma}\,A}a_{1})\to e% =e^{\prime}$

We do not add that contexts form a set as it is provable by induction on the context ().

Now we can hope for normalisation for this syntax, but the standard interpretation does not work anymore: the interpretation of $\mathsf{Ty}\,\mathit{\Gamma}$ would be $\llbracket\mathit{\Gamma}\rrbracket\to\mathsf{Type}$ , but then we cannot interpret $\mathsf{isSetTy}$ , as $\mathsf{Type}$ does not form a set. We have to limit ourselves to interpreting $\mathsf{Ty}\,\mathit{\Gamma}$ by $\llbracket\mathit{\Gamma}\rrbracket\to\mathsf{Prop}$ where $\mathsf{Prop}$ is defined as $(A:\mathsf{Type})\times\big((x\,y:A)\to x=y\big)$ . Alternatively, we can interpret $\mathsf{Ty}$ into an inductive-recursive universe as in [5, Section 6], but we cannot interpret the set-syntax in a univalent model. To fix this, we introduce a syntax where substitutions and terms are truncated to be sets, but types are only groupoid-truncated. To make types well-behaved, we add coherence laws which are equations between equations between types. These express that the substitution laws $\mathsf{U}[]$ , $\mathsf{El}[]$ and $\Pi[]$ commute with the functoriality laws $[\circ]$ , $[\mathsf{id}]$ . In the diagrams below, the vertical directions are the substitution laws and the horizontal directions are the functoriality laws.

Definition 7 (Groupoid-syntax ).

The groupoid-based syntax is the wild syntax (Definition 2) extended with the following higher equality constructors. Some of them are drawn as commutative diagrams.

In the types of $\mathsf{U}[\circ]$ and $\mathsf{U}[\mathsf{id}]$ above, $[{\circ}]^{\mathsf{U}}$ and $[\mathsf{id}]^{\mathsf{U}}$ abbreviate the following equality proofs. $[{\circ}]^{\mathsf{U}}$ is the dotted line in the left dependent square which is over the right square. $[\mathsf{id}]^{\mathsf{U}}$ is the dotted line in the upper dependent triangle which is over the lower triangle. As the bottom lines in the base square/triangle are reflexivities, $[{\circ}]^{\mathsf{U}}$ and $[\mathsf{id}]^{\mathsf{U}}$ are homogeneous equalities, but all the other lines in the upper shapes are heterogeneous. Fillers of the base shapes are written in their center, they are operations of the groupoid-syntax defined before. In Cubical Agda, the dotted lines are defined via heterogeneous composition. The $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}]^{\mathsf{U}}\mathsf{filler}$ operation is part of Definition 2.

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-% page-9.pdf2svg.svg}\end{matrix}\hskip 30.00005pt\begin{matrix}\includegraphics% {dagpub-standalone-combined-2026-01-06-12-07-19-page-10.pdf2svg.svg}\end{matrix}

In the types of $\Pi[{\circ}]$ and $\Pi[\mathsf{id}]$ above, we used the following abbreviations of paths. $[{\circ}^{+}]$ and $[\mathsf{id}^{+}]$ are the dotted lines in the upper triangles, which are over the lower triangles. The dotted lines are defined by composition. We also give names to the fillers of the upper triangles which will be used in Figures 2 and 3, respectively:

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-% page-11.pdf2svg.svg}\end{matrix}\begin{matrix}\includegraphics{dagpub-% standalone-combined-2026-01-06-12-07-19-page-12.pdf2svg.svg}\end{matrix}

This concludes the definition of the groupoid-syntax.

Notation 8.

We denote the components of the set-syntax by _S and the groupoid-syntax by _G subscripts, e.g. $\mathsf{Con}_{\mathsf{S}}$ and $\mathsf{Con}_{\mathsf{G}}$ .

We cannot redo the interpretation of Problem 4 because $\mathsf{Type}$ is not a groupoid, but we can refine it by interpreting types into $\mathsf{Set}$ .

Construction 9 (Set interpretation of the groupoid-syntax ).

We define the following functions mutually by pattern matching on the groupoid-syntax where $\mathsf{Set}:\equiv(X:\mathsf{Type})\times((e\,e^{\prime}:x_{0}=_{X}x_{1})\to e% =e^{\prime})$ .

	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Con}_{\mathsf{G}}\to\mathsf{Set}$	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Ty}_{\mathsf{G}}\,\mathit{\Gamma}\to\llbracket\mathit{% \Gamma}\rrbracket_{.1}\to\mathsf{Set}$
	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Sub}_{\mathsf{G}}\,\mathit{\Delta}\,\mathit{\Gamma}\to% \llbracket\mathit{\Delta}\rrbracket_{.1}\to\llbracket\mathit{\Gamma}\rrbracket% _{.1}\hskip 45.00006pt$	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Tm}_{\mathsf{G}}\,\mathit{\Gamma}\,A\to(\gamma:% \llbracket\mathit{\Gamma}\rrbracket_{.1})\to(\llbracket A\rrbracket\,\gamma)_{% .1}$

The cases for the constructors are analogous to the ones in Problem 4, with additional proofs of truncation-preservation: e.g. the empty context needs that $\top$ is a set, context extension needs that $\Sigma$ preserves set-truncation. $\mathsf{U}$ is interpreted by $X$ , $\mathsf{El}$ by $Y$ . We interpret the extra truncation constructors as follows: we prove $\mathsf{isGrpdTy}$ by the fact that $\mathsf{Set}$ forms a groupoid, while functions between sets are sets, which proves $\mathsf{isSetSub}$ and $\mathsf{isSetTm}$ . All 1-dimensional equalities and the 2-equalities $\mathsf{U}[\mathsf{id}]$ , $\mathsf{El}[\mathsf{id}]$ , $\Pi[\mathsf{id}]$ are interpreted by $\mathsf{refl}$ , while the 2-equalities $\mathsf{U}[\circ]$ , $\mathsf{El}[\circ]$ , $\Pi[\circ]$ use cubical filling because these include compositions in the formalisation (this could be avoided using the technique explained in Section 2).

The groupoid-syntax can be trivially interpreted into the set-syntax:

Construction 10 (Set-syntax interpretation of the groupoid-syntax ).

By pattern matching:

	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Con}_{\mathsf{G}}\to\mathsf{Con}_{\mathsf{S}}$	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Ty}_{\mathsf{G}}\,\mathit{\Gamma}\to\mathsf{Ty}_{\mathsf% {S}}\,\llbracket\mathit{\Gamma}\rrbracket$
	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Sub}_{\mathsf{G}}\,\mathit{\Delta}\,\mathit{\Gamma}\to% \mathsf{Sub}_{\mathsf{S}}\,\llbracket\mathit{\Delta}\rrbracket\,\llbracket% \mathit{\Gamma}\rrbracket\hskip 50.00008pt$	$\displaystyle\llbracket\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rrbracket$	$\displaystyle:\mathsf{Tm}_{\mathsf{S}}\,\mathit{\Gamma}\,A\to\mathsf{Tm}_{% \mathsf{S}}\,\llbracket\mathit{\Gamma}\rrbracket\,\llbracket A\rrbracket$

Everything is interpreted by the corresponding component in the set-syntax, except (i) $\mathsf{isGrpdTy}_{\mathsf{G}}$ is interpreted by applying cumulativity of truncation levels to $\mathsf{isSetTy}_{\mathsf{S}}$ ; (ii) the higher equalities $\mathsf{U}[{\circ}],\dots,\Pi[\mathsf{id}]$ are interpreted by $\mathsf{isSetTy}_{\mathsf{S}}$ .

4 $\upalpha$ -normalisation for the groupoid-syntax

In this section we prove that although elements of $\mathsf{Ty}_{\mathsf{G}}$ in the groupoid-syntax are only groupoid-truncated, they form a set. We define the set of $\upalpha$ -normal forms for $\mathsf{Ty}_{\mathsf{G}}$ , and then we show that every $\mathsf{Ty}_{\mathsf{G}}$ is a retract of its $\upalpha$ -normal forms. $\upalpha$ -normalisation is the process of eliminating explicit instantiations from types along the substitution laws for types.

4.1 $\upalpha$ -normal forms

Definition 11 ( $\upalpha$ -normal forms ).

$\upalpha$ -normal forms are given by the inductive family $\mathsf{NTy}$ which is defined mutually with the quote function $\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\urcorner$ . We overload constructor names and metavariables, but use brick red colour for disambiguation.

$\displaystyle\mathsf{NTy}$	$\displaystyle:\mathsf{Con}_{\mathsf{G}}\to\mathsf{Type}$	$\displaystyle\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\urcorner$	$\displaystyle:\mathsf{NTy}\,\mathit{\Gamma}\to\mathsf{Ty}_{\mathsf{G}}\,% \mathit{\Gamma}$
$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\mathsf{U}}}$	$\displaystyle:\mathsf{NTy}\,\mathit{\Gamma}$	$\displaystyle\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\urcorner$	$\displaystyle:\equiv\mathsf{U}_{\mathsf{G}}$
$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\mathsf{El}}}$	$\displaystyle:\mathsf{Tm}_{\mathsf{G}}\,\mathit{\Gamma}\,\mathsf{U}_{\mathsf{G% }}\to\mathsf{NTy}\,\mathit{\Gamma}$	$\displaystyle\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A}\urcorner$	$\displaystyle:\equiv\mathsf{El}_{\mathsf{G}}\,\hat{A}$
$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\Pi}}$	$\displaystyle:({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{A}}:\mathsf{NTy}\,\mathit{\Gamma})\to\mathsf{NTy}\,(% \mathit{\Gamma}\triangleright_{\mathsf{G}}\ulcorner{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\urcorner)% \to\mathsf{NTy}\,\mathit{\Gamma}\hskip 30.00005pt$	$\displaystyle\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}\urcorner$	$\displaystyle:\equiv\Pi_{\mathsf{G}}\,\ulcorner{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\urcorner\,% \ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{B}}\urcorner$

It is not obvious that $\upalpha$ -normal forms are a set because $\mathsf{NTy}$ is indexed by $\mathsf{Con}_{\mathsf{G}}$ which contains elements of $\mathsf{Ty}_{\mathsf{G}}$ for which at this point we do not know that it forms a set. $\mathsf{NTy}$ also includes non-normal terms (via ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{El}}}$ ), hence we cannot rely on decidability of equality and Hedberg’s theorem [36, Section 7.2]. However, we can still show the following.

Lemma 12 ().

$\mathsf{NTy}\,\mathit{\Gamma}$ forms a set.

Proof.

We use the encode-decode method [36] to characterise equality of $\mathsf{NTy}$ . The cover (or code) relation is defined by double-recursion on $\mathsf{NTy}$ , mutually with the decode function.

$\mathsf{Cover}:\mathsf{NTy}\,\mathit{\Gamma}\to\mathsf{NTy}\,\mathit{\Gamma}% \to\mathsf{Type}\hskip 105.00015pt\mathsf{decode}:\mathsf{Cover}\,{\color[rgb]% {0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A_{0}}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{1}}}\to{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{0}}}={\color% [rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A_{1}}}$
$\displaystyle\mathsf{Cover}\,{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\,$	$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\mathsf{U}}}$	$\displaystyle:\equiv\top$
$\displaystyle\mathsf{Cover}\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A_{0}})\,$	$\displaystyle({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A_{1}})$	$\displaystyle:\equiv\hat{A_{0}}=\hat{A_{1}}$
$\displaystyle\mathsf{Cover}\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{0}}}\,{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B_{0}}})\,$	$\displaystyle({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{1}}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B_{1}}})$	$\displaystyle:\equiv({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}% {rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{2}}}:\mathsf{Cover}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A_{0}}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{1}}})\times\mathsf{Cover}\,((% \mathsf{decode}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb% }{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{2}}})_{*}\,{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B_{0}}})\,{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B_{1}}}$
$\displaystyle\mathsf{Cover}\,\_$	$\displaystyle\_$	$\displaystyle:\equiv\bot$

The $\mathsf{decode}$ function is defined by double-induction on ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A_{0}}}$ and ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A_{1}}}$ . Again, by double induction on $\mathsf{NTy}$ , we prove that $\mathsf{Cover}$ is a proposition. By mutual induction on $\mathsf{NTy}$ , we prove that $\mathsf{Cover}$ is reflexive and decoding this reflexivity proof gives an identity (reflexivity) path.

\displaystyle\mathsf{reflCode}

\displaystyle:({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{A}}:\mathsf{NTy}\,\mathit{\Gamma})\to\mathsf{Cover}\,{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}

\displaystyle\mathsf{decRefl}

\displaystyle:({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{A}}:\mathsf{NTy}\,\mathit{\Gamma})\to\mathsf{decode}\,(% \mathsf{reflCode}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}})=\mathsf{refl}

We use these and J to define encode and prove that $\mathsf{decode}$ is a retraction:

\displaystyle\mathsf{encode}

\displaystyle:{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{A_{0}}}={\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{1}}}\to\mathsf{Cover}\,{\color% [rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A_{0}}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{1}}}

\displaystyle\mathsf{decEnc}

\displaystyle:({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{A_{2}}}:{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{0}}}={\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{1}}})\to% \mathsf{decode}\,(\mathsf{encode}\,{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{2}}})={\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{2}}}

As retractions preserve homotopy levels, from $\mathsf{Cover}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{0}}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{1}}}$ being a proposition, we obtain that ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A_{0}}}={\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}% {rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A_{1}}}$ is a proposition, hence $\mathsf{NTy}\,\mathit{\Gamma}$ is a set. $\hfill\blacktriangleleft$

4.2 $\upalpha$ -normalisation

We want to show that $\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\urcorner:\mathsf{NTy}\,% \mathit{\Gamma}\to\mathsf{Ty}_{\mathsf{G}}\,\mathit{\Gamma}$ is a retraction, which will imply that $\mathsf{Ty}_{\mathsf{G}}\,\mathit{\Gamma}$ is a set. For this, we define the other direction which is the normalisation function and its completeness.

Notation 13.

For the rest of this section, as we only talk about the groupoid-syntax, we do not write the _G subscripts, so $\mathsf{Ty}$ means $\mathsf{Ty}_{\mathsf{G}}$ , $\mathsf{U}$ means $\mathsf{U}_{\mathsf{G}}$ , and so on.

Problem 14 ( $\upalpha$ -normalisation ).

We define the following two functions by mutual induction on the groupoid-syntax.

\displaystyle\mathsf{norm}

\displaystyle:\mathsf{Ty}\,\mathit{\Gamma}\to\mathsf{NTy}\,\mathit{\Gamma}

\displaystyle\mathsf{compl}

\displaystyle:(A:\mathsf{Ty}\,\mathit{\Gamma})\to\ulcorner\mathsf{norm}\,A% \urcorner=A

Construction.

On $\mathsf{U}$ and $\mathsf{El}$ , the construction is trivial.

\displaystyle\mathsf{norm}\,\mathsf{U}

\displaystyle:\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\hskip 30.00005pt

\displaystyle\mathsf{norm}\,(\mathsf{El}\,\hat{A})

\displaystyle:\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A}

\displaystyle\mathsf{compl}\,\mathsf{U}

\displaystyle:\equiv\mathsf{refl}\hskip 30.00005pt

\displaystyle\mathsf{compl}\,(\mathsf{El}\,\hat{A})

\displaystyle:\equiv\mathsf{refl}

On $\Pi$ , we normalise recursively, but as $\mathsf{norm}\,B:\mathsf{NTy}\,(\mathit{\Gamma}\triangleright A)$ , we need to transport it over completeness of $A$ to obtain an $\mathsf{NTy}\,(\mathit{\Gamma}\triangleright\ulcorner\mathsf{norm}\,A\urcorner)$ :

	$\displaystyle\mathsf{norm}\,(\Pi\,A\,B):\equiv{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,(\mathsf% {norm}\,A)\,\big((\mathsf{compl}\,A)_{*}\,\mathsf{norm}\,B\big)$
	$\displaystyle\mathsf{compl}\,(\Pi\,A\,B):\ulcorner\mathsf{norm}\,(\Pi\,A\,B)\urcorner\equiv$
	$\displaystyle\hphantom{\mathsf{compl}\,(\Pi\,A\,B):{}}\Pi\,\ulcorner\mathsf{% norm}\,A\urcorner\,\ulcorner(\mathsf{compl}\,A)_{*}\,(\mathsf{norm}\,B)% \urcorner\overset{\mathsf{compl}\,A}{=}\Pi\,A\,\ulcorner\mathsf{norm}\,B% \urcorner\overset{\mathsf{compl}\,B}{=}\Pi\,A\,B$

To define $\mathsf{norm}$ on instantiated types, we need to instantiate normal forms. For this, we first show the following.

Problem 15 ().

$\mathsf{NTy}$ can be equipped with an instantiation operation $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ which is functorial, and $\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\urcorner$ is a “2-natural transformation”³³3We do not formally show that $\mathsf{Ty}$ and $\mathsf{NTy}$ form 2-functors, we use the phrase for intuition. into $\mathsf{Ty}$ , as follows (note the difference in colours for the overloaded names).

	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}:\mathsf{NTy}\,\mathit{\Gamma}% \to\mathsf{Sub}\,\mathit{\Delta}\,\mathit{\Gamma}\to\mathsf{NTy}\,\mathit{% \Delta}\hskip 13.99995pt{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\circ{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}:\forall{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,\gamma\,\delta\ldotp{\color[rgb]{0.72,0,0}\definecolor[named% ]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma\circ% \delta{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}={\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb% }{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\delta{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\hskip 13.99% 995pt{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}:\forall{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\ldotp{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}={\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb% }{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}$
	$\displaystyle\ulcorner\urcorner[]:\forall{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,\gamma\ldotp\ulcorner{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\urcorner[\gamma]=\ulcorner{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\urcorner$
	$\displaystyle\ulcorner\urcorner[\circ]:\forall{{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}}\,\gamma\,% \delta\ldotp\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-% 06-12-07-19-page-13.pdf2svg.svg}\end{matrix}\hskip 11.99998pt\ulcorner% \urcorner[\mathsf{id}]:\forall{{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}}\ldotp\begin{matrix}% \includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-page-14.pdf2% svg.svg}\end{matrix}$

Construction for Problem 15.

Instantiation of normal types is by mutual induction with naturality of $\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\urcorner$ . Instantiating ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{U}}}$ just changes the implicit context arguments, instantiating ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{El}}}$ means instantiating the term (which is an ordinary $\mathsf{Tm}_{\mathsf{G}}$ term, and is not normal), instantiating ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}$ is recursive:

\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\mathsf{U}}}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}

\displaystyle:\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\hskip 40.00006pt

\displaystyle({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A}){\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}

\displaystyle:\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,(\hat{A}[\gamma]^{% \mathsf{U}})\hskip 40.00006pt

\displaystyle({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}){\color[rgb% ]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}

\displaystyle:\equiv\Pi\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}})\,({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{% \ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}})

The operation $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}^{\ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor% [named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}% {0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ used in the codomain of $\Pi$ is defined as follows. It also comes with a filler equation.

	$\displaystyle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}^{\ulcorner+\urcorner}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$	$\displaystyle:\mathsf{NTy}\,(\mathit{\Gamma}\triangleright\ulcorner{\color[rgb% ]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\urcorner)\to(\gamma:\mathsf{Sub}\,\mathit{\Delta}\,\mathit{% \Gamma})\to\mathsf{NTy}\,(\mathit{\Delta}\triangleright\ulcorner{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\urcorner)$
	$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{\ulcorner+\urcorner}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}$	$\displaystyle:\equiv(\ulcorner\urcorner[]\,{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,\gamma)_{*}\,({\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{+}{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}})$
	${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{\ulcorner+\urcorner}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\mathsf{filler}:{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{+}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}=^{\ulcorner\urcorner[]\,{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,\gamma}{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{\ulcorner+\urcorner}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}$

Analogously to $[{\circ}^{+}]$ and $[\mathsf{id}^{+}]$ of Definition 7, we define their “normal substitution” versions ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}{\circ}^{+}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ and ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\mathsf{id}^{+}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ . Naturality is reusing the substitution law of the corresponding syntactic operation, and in the case of ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}$ , naturality for ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}$ and ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}$ are used (in the codomain of $\Pi$ , both $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}^{\ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor% [named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}% {0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ and its filler are used):

	$\displaystyle\ulcorner\urcorner[]\,{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\,\gamma$	$\displaystyle{}:\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\urcorner[\gamma]% \equiv\mathsf{U}[\gamma]\overset{\mathsf{U}[]\,\gamma}{=}\mathsf{U}\equiv% \ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\mathsf{U}}}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\urcorner$
	$\displaystyle\ulcorner\urcorner[]\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A})\,\gamma$	$\displaystyle{}:\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A}\urcorner[% \gamma]\equiv(\mathsf{El}\,\hat{A})[\gamma]\overset{\mathsf{El}[]\,\hat{A}\,% \gamma}{=}\mathsf{El}\,(\hat{A}[\gamma]^{\mathsf{U}})\equiv\ulcorner{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{(}}\mathsf{El}\,\hat{A}){\color[rgb]{0.72,0,0}\definecolor[named]% {pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\urcorner$
	$\displaystyle\ulcorner\urcorner[]\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}})\,\gamma$	$\displaystyle{}:\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}\urcorner[\gamma]\equiv(\Pi\,\ulcorner{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\urcorner\,% \ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{B}}\urcorner)[\gamma]\overset{\Pi[]\,\ulcorner{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\urcorner\,\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}\urcorner\,\gamma}{=}\Pi\,(% \ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{A}}\urcorner[\gamma])\,(\ulcorner{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}\urcorner[% \gamma^{+}])\overset{\ulcorner\urcorner[]\,{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}\,\gamma^{+}}{=}$
	$\hskip 50.00008pt\Pi\,(\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\urcorner[\gamma])\,\ulcorner{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{+}{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\urcorner\overset{\Pi\,(\ulcorner\urcorner[]\,{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,\gamma)\,\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{% \ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\mathsf{filler}\urcorner}{=}% \Pi\,\ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{A}}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\urcorner\,% \ulcorner{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{\ulcorner+\urcorner}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\urcorner\equiv\ulcorner({\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0% }\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0% }{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}){\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb% }{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\urcorner$

The functoriality equation ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}{\circ}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ and the 2-naturality square $\ulcorner\urcorner[\circ]$ are proven mutually by induction on $\mathsf{NTy}$ . The composition functor law for ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{U}}}$ is definitional, for ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{El}}}$ it reuses the functor law for terms of type $\mathsf{U}$ , for ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}$ it is recursive:

	$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{[}}{\circ}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\,% \gamma\,\delta$	$\displaystyle{}:{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}{\color[rgb]{0.72,0,0% }\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0% }{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma\circ% \delta{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\equiv{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{U}}}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}{\color[rgb]% {0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\delta{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$
	$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{[}}{\circ}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,% \hat{A})\,\gamma\,\delta$	$\displaystyle{}:({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb% }{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A}){\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\gamma\circ\delta{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\equiv{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,% (\hat{A}[\gamma\circ\delta]^{\mathsf{U}})\overset{[\circ]^{\mathsf{U}}\,\hat{A% }\,\gamma\,\delta}{=}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}% {rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,(\hat{A}[\gamma]^{% \mathsf{U}}[\delta]^{\mathsf{U}})\equiv({\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A}){% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\delta{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}$
	$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{[}}{\circ}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}})\,\gamma\,\delta$	$\displaystyle{}:({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb% }{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}}){\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb% }{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma\circ\delta{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}{\color[rgb]% {0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\gamma\circ\delta{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}})\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}{\color[rgb]% {0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}(\gamma\circ\delta)^{\ulcorner+\urcorner}{\color[rgb]{0.72,0,0% }\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0% }{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}})\overset{{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}\,({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}% {rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}{\circ}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,\gamma\,\delta)\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}{\circ}^{\ulcorner+\urcorner}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}\,\gamma\,\delta)}{=}$
		$\displaystyle\hphantom{{}:{}}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}{\color[rgb]% {0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\delta{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}})\,({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma^{% \ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\delta^{% \ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}})\equiv({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}){\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}% {0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\delta{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$

In the codomain part of the proof for ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}$ above, we used functoriality of the $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}^{\ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor% [named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}% {0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ operation which is defined by the dotted line (given by composition) in the following left square which is over the right square. We also give name to the filler of the left square.

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-% page-15.pdf2svg.svg}\end{matrix}

The $\ulcorner\urcorner[\circ]$ -squares for ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{U}}}$ and ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{El}}}$ are definitionally the same as $\mathsf{U}[\circ]$ and $\mathsf{El}[\circ]$ , respectively. We present the diagrammatic proof of $\mathsf{U}[\circ]$ for clarity, where double line means definitional equality. In this diagram, the inner and outer squares are definitionally equal. The square for ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}$ is more involved, we present it in Figure 2 in the Appendix.

	$\displaystyle{\ulcorner\urcorner[\circ]\,{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\,\gamma\,\delta% :\equiv\mathsf{U}[\circ]\,\gamma\,\delta}\hskip 40.00006pt{\begin{matrix}% \includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-page-16.pdf2% svg.svg}\end{matrix}}$
	$\displaystyle\ulcorner\urcorner[\circ]\,({\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A})\,% \gamma\,\delta:\equiv\mathsf{El}[\circ]\,\hat{A}\,\gamma\,\delta\text{, see % also Figure \ref{fig:El}}$
	$\displaystyle\ulcorner\urcorner[\circ]\,({\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0% }\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0% }{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{B}})\,\gamma\,\delta:\text{see Figure \ref{fig:picomp}}$

The functoriality equation ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ is proven by mutual induction on $\mathsf{NTy}$ .

	$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}:{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{U}}}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}\hskip 124.00012pt{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,% \hat{A}):({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,\hat{A}){\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathsf{id}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,(\hat{A}[\mathsf{% id}]^{\mathsf{U}})\overset{[\mathsf{id}]^{\mathsf{U}}\,\hat{A}}{=}{\color[rgb]% {0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\mathsf{El}}}\,\hat{A}$
	$\displaystyle{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}):({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}){\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathsf{id}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\equiv{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}{\color[rgb]% {0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}})\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}{\color[rgb]% {0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\mathsf{id}^{\ulcorner+\urcorner}{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}})\overset{{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}\,({\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}% {rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}})\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathsf{id}^% {\ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}% {rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}})}{=}{\color% [rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}$

In the codomain part of the proof for ${\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{\Pi}}$ above, we used functoriality of the $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}^{\ulcorner+\urcorner}{\color[rgb]{0.72,0,0}\definecolor% [named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}% {0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$ operation which is defined by the dotted line in the following upper triangle which is over the lower triangle. We also give a name to the filler of the upper triangle.

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-% page-17.pdf2svg.svg}\end{matrix}

The 2-naturality triangle $\ulcorner\urcorner[\mathsf{id}]$ is proven by induction on $\mathsf{NTy}$ as follows:

\displaystyle\ulcorner\urcorner[\mathsf{id}]\,{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{U}}}

\displaystyle:\equiv\mathsf{U}[\mathsf{id}]\hskip 50.00008pt

\displaystyle\ulcorner\urcorner[\mathsf{id}]\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\mathsf{El}}}\,% \hat{A})

\displaystyle:\equiv\mathsf{El}[\mathsf{id}]\,\hat{A}\hskip 50.00008pt

\displaystyle\ulcorner\urcorner[\mathsf{id}]\,({\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\Pi}}\,{\color[% rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{A}}\,{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{% rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}})

\displaystyle:\text{see Figure \ref{fig:piid}}

This finishes the construction for Problem 15. $\hfill\blacktriangleleft$ So far, we defined $\mathsf{norm}$ and $\mathsf{compl}$ on $\mathsf{U}$ , $\mathsf{El}$ and $\Pi$ . On substituted types, we define normalisation and its completeness as follows.

	$\displaystyle\mathsf{norm}\,(A[\gamma]):\equiv(\mathsf{norm}\,A){\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{[}}\gamma{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor% }{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{]}}$
	$\displaystyle\mathsf{compl}\,(A[\gamma]):\ulcorner\mathsf{norm}\,(A[\gamma])% \urcorner\equiv\ulcorner(\mathsf{norm}\,A){\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\gamma{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\urcorner\overset{\ulcorner\urcorner[]\,(\mathsf{norm}\,A)\,% \gamma}{=}\ulcorner\mathsf{norm}\,A\urcorner[\gamma]\overset{\mathsf{compl}\,A% }{=}A[\gamma]$

The action of $\mathsf{norm}$ on the functor laws is the corresponding functor law for instantiation of normal types, i.e. $\mathsf{norm}\,([{\circ}]\,A\,\gamma\,\delta):\equiv{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}{\circ}{% \color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\,(\mathsf{norm}\,A)\,\gamma\,\delta$ and $\mathsf{norm}\,([\mathsf{id}]\,A):\equiv{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{[}}\mathsf{id}{\color[rgb]{% 0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}% \pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}% {0.94}{0.28}{]}}\,(\mathsf{norm}\,A)$ . Completeness for the functor laws is the filling of the following two squares:

\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01-06-12-07-19-% page-18.pdf2svg.svg}\end{matrix}\begin{matrix}\includegraphics{dagpub-% standalone-combined-2026-01-06-12-07-19-page-19.pdf2svg.svg}\end{matrix}

The action of $\mathsf{norm}$ on the substitution laws for $\mathsf{U}$ and $\mathsf{El}$ is given by $\mathsf{refl}$ , and $\mathsf{compl}$ is given by trivial fillers for degenerate squares. The actions of $\mathsf{norm}$ and $\mathsf{compl}$ on $\Pi[]\,A\,B\,\gamma$ only involve naturality squares and fillers, they are presented in Figures 4 and 5 in the appendix.

The rest of the $\mathsf{Ty}$ -paths that $\mathsf{norm}$ and $\mathsf{compl}$ have to preserve are the 2-paths $\mathsf{U}[\circ]$ , $\mathsf{U}[\mathsf{id}]$ , $\mathsf{El}[\circ]$ , $\mathsf{El}[\mathsf{id}]$ , $\Pi[\circ]$ , $\Pi[\mathsf{id}]$ . As $\mathsf{norm}$ returns in a set, these are all trivial. The function $\mathsf{compl}$ produces an equality between elements of $\mathsf{Ty}$ , and as $\mathsf{Ty}$ is a groupoid, it trivially preserves 2-paths. Having defined $\mathsf{norm}$ and $\mathsf{compl}$ , we finished the construction for Problem 14. $\hfill\blacktriangleleft$

Theorem 16 ().

$\mathsf{Ty}_{\mathsf{G}}\,\mathit{\Gamma}$ is a set.

Proof.

Together, $\mathsf{norm}$ and $\mathsf{compl}$ witness that $\ulcorner\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\urcorner$ is a retraction, which preserves h-levels: as $\mathsf{NTy}\,\mathit{\Gamma}$ is a set, so is $\mathsf{Ty}\,\mathit{\Gamma}$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 17.

Stability of normalisation is also provable, but we do not need it in this paper.

5 Reaping the fruits

Problem 18 ().

The set-syntax is isomorphic to the groupoid-syntax.

Construction.

In Construction 10, we defined the map from the groupoid-syntax to the set-syntax. Now we define the opposite direction using that $\mathsf{Ty}_{\mathsf{G}}\,\mathit{\Gamma}$ is a set. The roundtrips are proven by two simple inductions. $\hfill\blacktriangleleft$

Construction 19 (Set interpretation of the set-syntax ).

We compose the groupoid-interpretation of the set syntax (Problem 18) and the set interpretation of the groupoid-syntax (Construction 9).

Groupoid CwFs are essentially algebras of the substitution calculus part of the groupoid-syntax (Definition 7), but we also include three coherence laws for types (the pentagon law $[\mathsf{ass}]$ and two identity triangles).

Definition 20 (Groupoid CwF, GCwF ).

An Ehrhard-style groupoid CwF is a 1-category (objects named $\mathsf{Con}:\mathsf{Type}$ , morphisms $\mathsf{Sub}:\mathsf{Con}\to\mathsf{Con}\to\mathsf{Set}$ ), a 2-presheaf of types (given by $\mathsf{Ty}:\mathsf{Con}\to\mathsf{Groupoid}$ , $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}[\mathord{\hskip 1.0pt\text{--}% \hskip 1.0pt}]:\mathsf{Ty}\,\mathit{\Gamma}\to\mathsf{Sub}\,\mathit{\Delta}\,% \mathit{\Gamma}\to\mathsf{Ty}\,\mathit{\Delta}$ , $[\circ]:A[\gamma\circ\delta]=A[\gamma][\delta]$ , $[\mathsf{id}]:A[\mathsf{id}]=A$ , $[\mathsf{ass}]$ , $[\mathsf{idl}]$ , $[\mathsf{idr}]$ as depicted below), a dependent presheaf of terms over types ( $\mathsf{Tm}:(\mathit{\Gamma}:\mathsf{Con})\to\mathsf{Ty}\,\mathit{\Gamma}\to% \mathsf{Set}$ , with instantiation and functor laws), with Ehrhard-style comprehension (operations $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\triangleright\mathord{\hskip 1.0pt% \text{--}\hskip 1.0pt}$ , $\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}^{+}$ , $\mathsf{p}$ , $\mathsf{q}$ , $\langle\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\rangle$ with 8 equations as in Definition 2).

	$\displaystyle[\mathsf{ass}]:\forall A\,\gamma\,\delta\,\theta\ldotp$	$\displaystyle[\mathsf{idl}]:\forall A\,\gamma\ldotp$	$\displaystyle[\mathsf{idr}]:\forall A\,\gamma\ldotp$
	$\displaystyle\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01% -06-12-07-19-page-20.pdf2svg.svg}\end{matrix}$	$\displaystyle\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01% -06-12-07-19-page-21.pdf2svg.svg}\end{matrix}$	$\displaystyle\begin{matrix}\includegraphics{dagpub-standalone-combined-2026-01% -06-12-07-19-page-22.pdf2svg.svg}\end{matrix}$

$\blacktriangleright$ Remark 21 ().

In any groupoid CwF, $[\mathsf{idl}]$ and $[\mathsf{idr}]$ are interderivable. The direction $[\mathsf{idl}]\to[\mathsf{idr}]$ is described in Figure 6 in the appendix. The same proof in the context of monoidal categories appears in [28, Theorem 7].

Proposition 22 ().

In the groupoid-syntax (Definition 7), the laws $[\mathsf{ass}]$ , $[\mathsf{idl}]$ and $[\mathsf{idr}]$ are admissible.

Proof.

Direct consequence of Theorem 16. $\hfill\blacktriangleleft$

6 Conclusions

We have presented a basic coherence theorem for GCwF, enabling the interpretation of the usual decidable intrinsic syntax of type theory within models based on categories where the objects do not form a set, such as the set model. Notably, we have achieved this without relying on normalisation for the groupoid syntax or invoking Hedberg’s theorem. Furthermore, our method is adaptable, in principle, to type theories without decidable equality. An interesting feature of our approach is that it eliminates the need to explicitly incorporate the usual coherence laws for 2-categories (such as the pentagon law) into the syntax; these laws are admissible in our groupoid-syntax.

Despite these advancements, several significant challenges remain. For instance, we aim to extend this framework to include a univalent universe of propositions (i.e. $\mathsf{Prop}$ with propositional extensionality). We also seek to address univalence for types without introducing an additional universe, thereby demonstrating that univalence can be soundly supported in this setting.

The addition of universes, even a minimal one such as a universe of Booleans with large eliminations, would require a shift in our methodology and might necessitate term normalisation. Extending the framework to accommodate multiple universes would inevitably demand a move to higher dimensions, introducing further complexity.

Our groupoid-syntax can be seen as the GCwF with $\Pi$ freely generated from a set and a family over it. We would like to support more interesting generating data, i.e. generating data which can refer to the GCwF structure while being defined.

Finally, we would like to revisit the longstanding problem of modeling semi-simplicial types within this context. One potential direction is to extend our current recursive treatment of substitution and substitution-related coherence laws, using these as a foundation to systematically derive higher coherence conditions.

References

[1] Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., 2(POPL):23:1–23:29, 2018. doi:10.1145/3158111.
[2] Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet. Martin-Löf à la Coq. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 230–245. ACM, 2024. doi:10.1145/3636501.3636951.
[3] Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 21:1–21:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPIcs.CSL.2016.21.
[4] Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus. Partiality, revisited - the partiality monad as a quotient inductive-inductive type. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 534–549, 2017. doi:10.1007/978-3-662-54458-7_31.
[5] Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18–29. ACM, 2016. doi:10.1145/2837614.2837638.
[6] Thorsten Altenkirch and Ambrus Kaposi. Normalisation by evaluation for type theory, in type theory. Logical methods in computer science, 13, 2017. doi:10.23638/LMCS-13(4:1)2017.
[7] Thorsten Altenkirch and Ambrus Kaposi. A container model of type theory. In Henning Basold, editor, 27th International Conference on Types for Proofs and Programs, TYPES 2021. Universiteit Leiden, 2021. URL: https://types21.liacs.nl/download/a-container-model-of-type-theory/.
[8] Thorsten Altenkirch and Luis Scoccola. The integers as a higher inductive type. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 67–73. ACM, 2020. doi:10.1145/3373718.3394760.
[9] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. Math. Struct. Comput. Sci., 33(8):688–743, 2023. doi:10.1017/S0960129523000130.
[10] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications - ERRATUM. Math. Struct. Comput. Sci., 34(1):80, 2024. doi:10.1017/S096012952300021X.
[11] Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. https://github.com/UniMath/SymmetryBook. Commit: ec9be72.
[12] Rafaël Bocquet. Strictification of weakly stable type-theoretic structures using generic contexts. In Henning Basold, Jesper Cockx, and Silvia Ghilezan, editors, 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference), volume 239 of LIPIcs, pages 3:1–3:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.TYPES.2021.3.
[13] Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with Families: Unityped, Simply Typed, and Dependently Typed, pages 135–180. Springer International Publishing, Cham, 2021. doi:10.1007/978-3-030-66545-6_5.
[14] Evan Cavallo and Robert Harper. Higher inductive types in cubical computational type theory. Proc. ACM Program. Lang., 3(POPL):1:1–1:27, 2019. doi:10.1145/3290314.
[15] James Chapman. Type theory should eat itself. In Andreas Abel and Christian Urban, editors, Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008, volume 228 of Electronic Notes in Theoretical Computer Science, pages 21–36. Elsevier, 2008. doi:10.1016/J.ENTCS.2008.12.114.
[16] Pierre Clairambault and Peter Dybjer. The biequivalence of locally cartesian closed categories and martin-löf type theories. Math. Struct. Comput. Sci., 24(6), 2014. doi:10.1017/S0960129513000881.
[17] Thierry Coquand. Generalised algebraic presentation of type theory, 2020. URL: https://www.cse.chalmers.se/˜coquand/cwf2.pdf.
[18] Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 255–264. ACM, 2018. doi:10.1145/3209108.3209197.
[19] Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, volume 4502 of Lecture Notes in Computer Science, pages 93–109. Springer, 2006. doi:10.1007/978-3-540-74464-1_7.
[20] Tim Lukas Diezel and Sergey Goncharov. Towards constructive hybrid semantics. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 24:1–24:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.FSCD.2020.24.
[21] Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120–134. Springer, 1995. doi:10.1007/3-540-61780-9_66.
[22] Thomas Ehrhard. Une sémantique catégorique des types dépendents. PhD thesis, Université Paris VII, 1988.
[23] Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 427–441. Springer, 1994. doi:10.1007/BFB0022273.
[24] Ambrus Kaposi. Re: Separate definition of constructors?, May 2019. Email message to the Agda mailing list. URL: https://lists.chalmers.se/pipermail/agda/2019/011176.html.
[25] Ambrus Kaposi and András Kovács. Signatures and induction principles for higher inductive-inductive types. Log. Methods Comput. Sci., 16(1), 2020. doi:10.23638/LMCS-16(1:10)2020.
[26] Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL):2:1–2:24, 2019. doi:10.1145/3290315.
[27] Ambrus Kaposi and Jakob von Raumer. A syntax for mutual inductive families. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 23:1–23:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.FSCD.2020.23.
[28] G. M. Kelly. On MacLane’s conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra, 1(4):397–402, 1964. doi:10.1016/0021-8693(64)90018-3.
[29] Nicolai Kraus. Internal $\infty$ -categorical models of dependent type theory: Towards 2LTT eating HoTT. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470667.
[30] Nicolai Kraus and Thorsten Altenkirch. Free higher groups in homotopy type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 599–608. ACM, 2018. doi:10.1145/3209108.3209183.
[31] Peter LeFanu Lumsdaine and Michael A. Warren. The local universes model: An overlooked coherence construction for dependent type theories. ACM Trans. Comput. Log., 16(3):23:1–23:31, 2015. doi:10.1145/2754931.
[32] Stefano Piceghello. Coherence for monoidal groupoids in HoTT. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1–8:20, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.TYPES.2019.8.
[33] Christian Sattler. Semantics of signatures for higher inductive-inductive types (HIITs) in complete Segal types, 2019. Notes on the author’s website. URL: https://www.cse.chalmers.se/˜sattler/docs/hits.
[34] Mike Shulman. Homotopy type theory should eat itself (but so far, it’s too big to swallow), 2014. Blog post on the Homotopy Type Theory website. URL: https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/.
[35] Taichi Uemura. Normalization and coherence for $\infty$ -type theories. CoRR, abs/2212.11764, 2022. doi:10.48550/arXiv.2212.11764.
[36] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
[37] Niels van der Weide. The internal languages of univalent categories. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 112–126. IEEE, 2025. doi:10.1109/LICS65433.2025.00016.
[38] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program., 31:e8, 2021. doi:10.1017/S0956796821000034.
[39] Vladimir Voevodsky. A C-system defined by a universe category, 2015. arXiv:1409.7925.
[40] David Wärn. Path spaces of pushouts, 2024. arXiv:2402.12339.

Appendix A More diagrams

Figure 1: This diagram is the proof

\ulcorner\urcorner[\circ]\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\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]\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\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}]\,({\color[rgb]{0.72,0,0}\definecolor[named]{% pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}% \pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\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{\color[rgb]{0.72,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{% 0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill% {0}{0.89}{0.94}{0.28}{A}}\urcorner\,\ulcorner{\color[rgb]{0.72,0,0}% \definecolor[named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}% {0.89}{0.94}{0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{B}}\urcorner

for readability.

Figure 4: Normalisation on the substitution law for

\Pi

acts as follows:

\mathsf{norm}\,(\Pi[]\,A\,B\,\gamma):\equiv{\color[rgb]{0.72,0,0}\definecolor[% named]{pgfstrokecolor}{rgb}{0.72,0,0}\pgfsys@color@cmyk@stroke{0}{0.89}{0.94}{% 0.28}\pgfsys@color@cmyk@fill{0}{0.89}{0.94}{0.28}{\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 4.

Figure 6: Proof that

[\mathsf{idl}]

implies

[\mathsf{idr}]

in any groupoid CwF (Definition 20).

[bib.bib1] [1] Andreas Abel, Joakim Öhman, and Andrea Vezzosi. Decidability of conversion for type theory in type theory. Proc. ACM Program. Lang., 2(POPL):23:1–23:29, 2018. doi:10.1145/3158111.

[bib.bib2] [2] Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard, Pierre-Marie Pédrot, and Loïc Pujet. Martin-Löf à la Coq. In Amin Timany, Dmitriy Traytel, Brigitte Pientka, and Sandrine Blazy, editors, Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2024, London, UK, January 15-16, 2024, pages 230–245. ACM, 2024. doi:10.1145/3636501.3636951.

[bib.bib3] [3] Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 21:1–21:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPIcs.CSL.2016.21.

[bib.bib4] [4] Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus. Partiality, revisited - the partiality monad as a quotient inductive-inductive type. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 534–549, 2017. doi:10.1007/978-3-662-54458-7_31.

[bib.bib5] [5] Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18–29. ACM, 2016. doi:10.1145/2837614.2837638.

[bib.bib6] [6] Thorsten Altenkirch and Ambrus Kaposi. Normalisation by evaluation for type theory, in type theory. Logical methods in computer science, 13, 2017. doi:10.23638/LMCS-13(4:1)2017.

[bib.bib7] [7] Thorsten Altenkirch and Ambrus Kaposi. A container model of type theory. In Henning Basold, editor, 27th International Conference on Types for Proofs and Programs, TYPES 2021. Universiteit Leiden, 2021. URL: https://types21.liacs.nl/download/a-container-model-of-type-theory/.

[bib.bib8] [8] Thorsten Altenkirch and Luis Scoccola. The integers as a higher inductive type. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 67–73. ACM, 2020. doi:10.1145/3373718.3394760.

[bib.bib9] [9] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. Math. Struct. Comput. Sci., 33(8):688–743, 2023. doi:10.1017/S0960129523000130.

[bib.bib10] [10] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications - ERRATUM. Math. Struct. Comput. Sci., 34(1):80, 2024. doi:10.1017/S096012952300021X.

[bib.bib11] [11] Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, and Daniel R. Grayson. Symmetry. https://github.com/UniMath/SymmetryBook. Commit: ec9be72.

[bib.bib12] [12] Rafaël Bocquet. Strictification of weakly stable type-theoretic structures using generic contexts. In Henning Basold, Jesper Cockx, and Silvia Ghilezan, editors, 27th International Conference on Types for Proofs and Programs, TYPES 2021, June 14-18, 2021, Leiden, The Netherlands (Virtual Conference), volume 239 of LIPIcs, pages 3:1–3:23. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPIcs.TYPES.2021.3.

[bib.bib13] [13] Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with Families: Unityped, Simply Typed, and Dependently Typed, pages 135–180. Springer International Publishing, Cham, 2021. doi:10.1007/978-3-030-66545-6_5.

[bib.bib14] [14] Evan Cavallo and Robert Harper. Higher inductive types in cubical computational type theory. Proc. ACM Program. Lang., 3(POPL):1:1–1:27, 2019. doi:10.1145/3290314.

[bib.bib15] [15] James Chapman. Type theory should eat itself. In Andreas Abel and Christian Urban, editors, Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008, volume 228 of Electronic Notes in Theoretical Computer Science, pages 21–36. Elsevier, 2008. doi:10.1016/J.ENTCS.2008.12.114.

[bib.bib16] [16] Pierre Clairambault and Peter Dybjer. The biequivalence of locally cartesian closed categories and martin-löf type theories. Math. Struct. Comput. Sci., 24(6), 2014. doi:10.1017/S0960129513000881.

[bib.bib17] [17] Thierry Coquand. Generalised algebraic presentation of type theory, 2020. URL: https://www.cse.chalmers.se/˜coquand/cwf2.pdf.

[bib.bib18] [18] Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 255–264. ACM, 2018. doi:10.1145/3209108.3209197.

[bib.bib19] [19] Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Thorsten Altenkirch and Conor McBride, editors, Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers, volume 4502 of Lecture Notes in Computer Science, pages 93–109. Springer, 2006. doi:10.1007/978-3-540-74464-1_7.

[bib.bib20] [20] Tim Lukas Diezel and Sergey Goncharov. Towards constructive hybrid semantics. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 24:1–24:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.FSCD.2020.24.

[bib.bib21] [21] Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120–134. Springer, 1995. doi:10.1007/3-540-61780-9_66.

[bib.bib22] [22] Thomas Ehrhard. Une sémantique catégorique des types dépendents. PhD thesis, Université Paris VII, 1988.

[bib.bib23] [23] Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Leszek Pacholski and Jerzy Tiuryn, editors, Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, volume 933 of Lecture Notes in Computer Science, pages 427–441. Springer, 1994. doi:10.1007/BFB0022273.

[bib.bib24] [24] Ambrus Kaposi. Re: Separate definition of constructors?, May 2019. Email message to the Agda mailing list. URL: https://lists.chalmers.se/pipermail/agda/2019/011176.html.

[bib.bib25] [25] Ambrus Kaposi and András Kovács. Signatures and induction principles for higher inductive-inductive types. Log. Methods Comput. Sci., 16(1), 2020. doi:10.23638/LMCS-16(1:10)2020.

[bib.bib26] [26] Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL):2:1–2:24, 2019. doi:10.1145/3290315.

[bib.bib27] [27] Ambrus Kaposi and Jakob von Raumer. A syntax for mutual inductive families. In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 23:1–23:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.FSCD.2020.23.

[bib.bib28] [28] G. M. Kelly. On MacLane’s conditions for coherence of natural associativities, commutativities, etc. Journal of Algebra, 1(4):397–402, 1964. doi:10.1016/0021-8693(64)90018-3.

[bib.bib29] [29] Nicolai Kraus. Internal $\infty$ -categorical models of dependent type theory: Towards 2LTT eating HoTT. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1–14. IEEE, 2021. doi:10.1109/LICS52264.2021.9470667.

[bib.bib30] [30] Nicolai Kraus and Thorsten Altenkirch. Free higher groups in homotopy type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 599–608. ACM, 2018. doi:10.1145/3209108.3209183.

[bib.bib31] [31] Peter LeFanu Lumsdaine and Michael A. Warren. The local universes model: An overlooked coherence construction for dependent type theories. ACM Trans. Comput. Log., 16(3):23:1–23:31, 2015. doi:10.1145/2754931.

[bib.bib32] [32] Stefano Piceghello. Coherence for monoidal groupoids in HoTT. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs (TYPES 2019), volume 175 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1–8:20, Dagstuhl, Germany, 2020. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/LIPIcs.TYPES.2019.8.

[bib.bib33] [33] Christian Sattler. Semantics of signatures for higher inductive-inductive types (HIITs) in complete Segal types, 2019. Notes on the author’s website. URL: https://www.cse.chalmers.se/˜sattler/docs/hits.

[bib.bib34] [34] Mike Shulman. Homotopy type theory should eat itself (but so far, it’s too big to swallow), 2014. Blog post on the Homotopy Type Theory website. URL: https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/.

[bib.bib35] [35] Taichi Uemura. Normalization and coherence for $\infty$ -type theories. CoRR, abs/2212.11764, 2022. doi:10.48550/arXiv.2212.11764.

[bib.bib36] [36] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.

[bib.bib37] [37] Niels van der Weide. The internal languages of univalent categories. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 112–126. IEEE, 2025. doi:10.1109/LICS65433.2025.00016.

[bib.bib38] [38] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program., 31:e8, 2021. doi:10.1017/S0956796821000034.

[bib.bib39] [39] Vladimir Voevodsky. A C-system defined by a universe category, 2015. arXiv:1409.7925.

[bib.bib40] [40] David Wärn. Path spaces of pushouts, 2024. arXiv:2402.12339.

The Groupoid-Syntax of Type Theory Is a Set

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

Supplementary Material:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Contributions.

Structure of the paper.

Related work.

2 Metatheory and formalisation

3 Variants of the syntax and the set interpretation

Parameter 1.

Definition 2 (Wild syntax ).

Example 3 (Using the wild syntax ).

Problem 4 (Type interpretation of the wild syntax ).

Construction.

Proposition 5 ().

Proof.

Definition 6 (Set-syntax ).

Definition 7 (Groupoid-syntax ).

Notation 8.

Construction 9 (Set interpretation of the groupoid-syntax ).

Construction 10 (Set-syntax interpretation of the groupoid-syntax ).

4 𝛂-normalisation for the groupoid-syntax

4.1 𝛂-normal forms

Definition 11 (α-normal forms ).

Lemma 12 ().

Proof.

4.2 𝛂-normalisation

Notation 13.

Problem 14 (α-normalisation ).

Construction.

Problem 15 ().

Construction for Problem 15.

Theorem 16 ().

Proof.

▶ Remark 17.

5 Reaping the fruits

Problem 18 ().

Construction.

Construction 19 (Set interpretation of the set-syntax ).

Definition 20 (Groupoid CwF, GCwF ).

▶ Remark 21 ().

Proposition 22 ().

Proof.

6 Conclusions

References

Appendix A More diagrams

4 $\upalpha$ -normalisation for the groupoid-syntax

4.1 $\upalpha$ -normal forms

Definition 11 ( $\upalpha$ -normal forms ).

4.2 $\upalpha$ -normalisation

Problem 14 ( $\upalpha$ -normalisation ).

$\blacktriangleright$ Remark 17.

$\blacktriangleright$ Remark 21 ().