# A parametricity-based formalization of semi-simplicial and semi-cubical sets

Hugo Herbelin, Ramkumar Ramachandra

<figure><img src="image_1.png" /></figure>

To cite this version:

Hugo Herbelin, Ramkumar Ramachandra. A parametricity-based formalization of semi-simplicial and semi-cubical sets. 2023. hal-03963929v2

HAL Id: hal-03963929

https://inria.hal.science/hal-03963929v2

Preprint submitted on 31 Dec 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License
<figure><img src="image_1.png" /></figure>

HAL
open science

# A parametricity-based formalization of semi-simplicial and semi-cubical sets

Hugo Herbelin, Ramkumar Ramachandra

► To cite this version:

Hugo Herbelin, Ramkumar Ramachandra. A parametricity-based formalization of semi-simplicial and semi-cubical sets. 2023. hal-03963929v4

HAL Id: hal-03963929

https://inria.hal.science/hal-03963929v4

Preprint submitted on 20 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License
# A parametricity-based formalization of semi-simplicial and semi-cubical sets

Hugo Herbelin

Université Paris-Cité, Inria, CNRS, IRIF, Paris

Hugo.Herbelin@inria.fr

Ramkumar Ramachandra

Université Paris-Cité (2020-2022), Unaffiliated

r@artagnon.com

## Abstract

Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alternative definition, where the set of n-simplices or n-cubes are instead regrouped into the families of the fibers over their faces, leading to a characterization we call indexed. Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds parametricity, respectively in its unary and binary variants. We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq.

# I INTRODUCTION

## Fibered vs indexed presentation of semi-simplicial and semi-cubical sets

A family of sets can commonly be represented in two ways: as a family properly speaking, indexed by the elements of a given set S, or as a set T together with a map from T to S, which specifies for each element of T its dependency on S. In the former case, we call it an indexed presentation. In the latter case, the set associated to a given element of S is the fiber of this element, so we call it a fibered presentation. The two presentations are equivalent and the equivalence can be phrased concisely in the language of homotopy type theory [The13] as the fibered/indexed equivalenceª.

$$ (\text{fibered}) \quad (\Sigma T : \mathbf{HSet}.(T \to S)) \simeq (S \to \mathbf{HSet}) \quad (\text{indexed}) $$

Here, HSet represents in homotopy type theory the subset of types within a given universe where equality of any two elements has at most one proof.

A presheaf on a category is a family of sets indexed by the object of the category with maps indexed by the morphisms. As such, it lives on the indexed side of the equivalence, contrasting with the fibered side, where we have discrete Grothendieck fibrations [LR20]. However, there are situations where a presheaf can also be seen as living on the fibered side of the equivalence. This happens when the indexing category is direct, or has a downwards-well-founded collection of non-identity morphisms. Let us consider, for instance, the case of a semi-cubical set [GM03, BM17] presented with 2n face maps from the set of n-cubes to the set of (n - 1)-cubes. Formulated in type theory, the corresponding presheaf definition of a semi-cubical set prescribes a family of sets and face maps between them as follows.

$$ X_0 : \mathbf{HSet} \quad \begin{array}{l} \leftarrow \partial^R - \\ \leftarrow \partial^L - \end{array} \quad X_1 : \mathbf{HSet} \quad \begin{array}{l} \leftarrow \partial^{*R} - \\ \leftarrow \partial^{*L} - \\ \leftarrow \partial^{*R*} - \\ \leftarrow \partial^{*L*} - \end{array} \quad X_2 : \mathbf{HSet} \quad \dots $$

<footnote>ªIn an informal discussion, alternative nomenclatures were proposed: fibration/family equivalence and unbundled/bundled equivalence. The fibered/indexed nomenclature echoes the Grothendieck construction of fibered categories from indexed categories. The most elementary instance of the equivalence, with Type instead of HSet, is sometimes called “Grothendieck construction for dummies”, and its proof requires univalence [The13].</footnote>
# A parametricity-based formalization of semi-simplicial and semi-cubical sets

Hugo Herbelin

Université Paris-Cité, Inria, CNRS, IRIF, Paris

Hugo.Herbelin@inria.fr

Ramkumar Ramachandra

Université Paris-Cité (2020-2022), Unaffiliated

r@artagnon.com

## Abstract

Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alternative definition, where the set of *n*-simplices or *n*-cubes are instead regrouped into the families of the fibres over their faces, leading to a characterization we call *indexed*. Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds parametricity, respectively in its unary and binary variants. We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq.

# I INTRODUCTION

## Fibred vs indexed presentation of semi-simplicial and semi-cubical sets

A family of sets can commonly be represented in two ways: as a family properly speaking, indexed by the elements of a given set $S$, or as a set $T$ together with a map from $T$ to $S$, which specifies for each element of $T$ its dependency on $S$. In the former case, we call it an *indexed* presentation. In the latter case, the set associated to a given element of $S$ is the fibre of this element, so we call it a *fibred* presentation. The two presentations are equivalent and the equivalence can be phrased concisely in the language of homotopy type theory [The13] as the fibred/indexed equivalenceª.

$$ (\text{fibred}) \quad (\Sigma T : \mathbf{HSet}.(T \to S)) \simeq (S \to \mathbf{HSet}) \quad (\text{indexed}) $$

Here, $\mathbf{HSet}$ represents in homotopy type theory the subset of types within a given universe where equality of any two elements has at most one proof.

A *presheaf* on a category is a family of sets indexed by the object of the category with maps indexed by the morphisms. As such, it lives on the indexed side of the equivalence, contrasting with the fibred side, where we have *discrete Grothendieck fibrations* [LR20]. However, there are situations where a presheaf can also be seen as living on the fibred side of the equivalence. This happens when the indexing category is *direct*, or has a downwards-well-founded collection of non-identity morphisms. Let us consider, for instance, the case of a semi-cubical set [GM03, BM17] presented with $2n$ face maps from the set of $n$-cubes to the set of $(n-1)$-cubes. Formulated in type theory, the corresponding presheaf definition of a semi-cubical set prescribes a family of sets and face maps between them as follows.

$$ X_0 : \mathbf{HSet} \quad \begin{array}{l} \leftarrow \partial^R \\ \leftarrow \partial^L \end{array} \quad X_1 : \mathbf{HSet} \quad \begin{array}{l} \leftarrow \partial^{*R} \\ \leftarrow \partial^{*L} \\ \leftarrow \partial^{*R^*} \\ \leftarrow \partial^{*L^*} \end{array} \quad X_2 : \mathbf{HSet} \quad \dots $$

<footnote>ªIn an informal discussion, alternative nomenclatures were proposed: fibration/family equivalence and unbundled/bundled equivalence. The fibred/indexed nomenclature echoes the Grothendieck construction of fibred categories from indexed categories. The most elementary instance of the equivalence, with Type instead of $\mathbf{HSet}$, is sometimes called “Grothendieck construction for dummies”, and its proof requires univalence [The13].</footnote>
up to cubical faces identities. Here, $X_1$ can be seen as a family over $X_0 \times X_0$, and $X_2$ can be seen as a family over $X_1 \times X_1 \times X_1 \times X_1$, in the fibered presentation. This suggests an alternative indexed presentation of the presheaf as a stratified sequence of families indexed by families of lower rank, taking into account the coherence conditions to prevent duplications. Formulated in type theory, it takes the form:

$$ \begin{array}{l} X_0 : \qquad \mathbf{HSet} \\ X_1 : \qquad X_0 \times X_0 \to \mathbf{HSet} \\ X_2 : \Piabcd. \quad X_1(a,b) \times X_1(c,d) \times X_1(a,c) \times X_1(b,d) \to \mathbf{HSet} \\ \dots \end{array} $$

The idea for such an indexed presentation of presheaves over a direct category was mentioned at the Univalent Foundations year in the context of defining semi-simplicial types$^b$. A few constructions have been proposed since then. The first construction by [Voe12] relies on the presentation of semi-simplicial sets as a presheaf over increasing injective maps between finite ordinals. The second, by [Her15]$^c$ formalized in the Coq proof assistant, relies on the presentation of semi-simplicial sets as a presheaf over face maps. Another by [PL15] formalized in an emulation of logic-enriched homotopy type theory in the Plastic proof assistant, and yet another by [ACK17] formalized in an emulation of a two-level type theory in the Agda proof assistant$^d$, rely on the presentation of the semi-simplicial category from increasing injective functions over finite ordinals.

The indexed definition of a presheaf over a direct category is technically more involved than the presheaf definition, as it requires hard-wiring in the structure the dependencies between elements of the sets of the presheaf, including the coherence conditions between these dependencies, such as taking the *i*-th face of the *j*-th face of a *n*-simplex being the same as taking the (*j* − 1)-th face of the *i*-th face (when *j* > *i*). However, exhibiting a concrete instance of a presheaf in indexed form only requires providing the families, since the responsibility of defining maps and showing the coherence conditions is already accounted for in the definition of the structure.

## Reynolds parametricity and its unary and binary variants

In the context of functional programming, Reynolds parametricity ([Rey83]) interprets types as relations characterizing the observational behavior of programs of this type. More generally, families over a product of sets, or *correspondences*, can be used in place of relations. Parametricity can then be iterated, and relying on the fibered presentation of correspondences as spans, it has been noted that iterated Reynolds parametricity has the structure of a cubical set [AK15, Mou16, JS17, Moe21, Moe22]. We obtain a *unary* variant of Reynolds *binary* parametricity by using predicates or families instead of relations or correspondences, and this is a form of realizability [BM12, Las14, Mou16]. It has then been noted that iterated unary parametricity has the structure of an augmented simplicial set$^e$. This suggests that the definition of augmented semi-simplicial sets and semi-cubical sets can both be seen as instances of a more general construction, which we call *ν*-sets, of presheaves over a *ν*-semi-shape category made of words of some cardinal $ν + 1$, where $ν = 1$ gives augmented semi-simplicial sets and $ν = 2$ gives semi-cubical sets.

## Contribution

The main contribution of the paper is to describe the details of a recipe that uniformly characterizes unary and binary iterated parametricity in indexed form, and to derive from it a new indexed presentation, called indexed *ν*-sets, of augmented semi-simplicial and semi-cubical sets.

Our work is a step in the direction of the program initiated in [AK15] to develop parametricity-based models of parametric type theory [BCM15, NVD17, CH20] and cubical type theory [BCH13, CCHM18, ABC$^+$21], which are closer to the syntax of type theory, and are likely to better reflect the definitional properties of type theory than presheaf-based cubical sets would. For example, consider the loss of definitional properties when interpreting “indexed” dependent types of type theory as “fibrations” in models such as locally cartesian closed categories [CGH14].

Our mechanization can be found at github.com/artagnon/bonak. The construction was conceived in Summer 2019, and the mechanization began in late 2019. A sketch of the construction was presented at the 2020 HoTT-UF workshop, and the completion of the mechanization was reported at the TYPES 2022 conference.

<footnote>$^b$ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory</footnote>

<footnote>$^c$In hindsight, the title of the paper “A dependently-typed construction of semi-simplicial types” is somewhat confusing: it implicitly claimed to construct semi-simplicial types, but the construction was done in a type theory with Uniqueness of Identity Proofs. Consequentially, what was really obtained was an indexed presentation of semi-simplicial sets. The confusion was however, common at the time.</footnote>

<footnote>$^d$github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/STypes.agda</footnote>

<footnote>$^e$Private communication with Hugo Moeneclaey and Thorsten Altenkirch.</footnote>
up to cubical faces identities. Here, $X_1$ can be seen as a family over $X_0 \times X_0$, and $X_2$ can be seen as a family over $X_1 \times X_1 \times X_1 \times X_1$, in the fibred presentation, together with coherence conditions between the $X_1$ seen as families over $X_0 \times X_0$. This suggests an alternative indexed presentation of the presheaf as a stratified sequence of families indexed by families of lower rank, taking into account those coherence conditions to prevent duplications. Formulated in type theory, it takes the form:

$$ 
\begin{align*}
X_0 & : \mathbf{HSet} \\
X_1 & : X_0 \times X_0 \rightarrow \mathbf{HSet} \\
X_2 & : \Pi \mathit{abcd}. X_1(a, b) \times X_1(c, d) \times X_1(a, c) \times X_1(b, d) \rightarrow \mathbf{HSet} \\
\dots
\end{align*}
$$

The idea for such an indexed presentation of presheaves over a direct category was mentioned at the Universal Foundations year in the context of defining semi-simplicial types<sup>b</sup>. A few constructions have been proposed since then. The first construction by [Voe12] relies on the presentation of semi-simplicial sets as a presheaf over increasing injective maps between finite ordinals. The second, by [Her15]<sup>c</sup> formalized in the Coq proof assistant, relies on the presentation of semi-simplicial sets as a presheaf over face maps. Another by [PL15] formalized in an emulation of logic-enriched homotopy type theory in the Plastic proof assistant, and yet another by [ACK16] formalized in an emulation of a two-level type theory in the Agda proof assistant<sup>d</sup>, rely, like in Voevodsky, on the presentation of the semi-simplicial category from increasing injective maps between finite ordinals. The latter constructions, besides being stated as providing semi-simplicial types (thanks to an extension of the type theory), are particularly concise, taking advantage of a definition of increasing injective maps between finite ordinals as type-theoretic functions to inherit the associativity of composition directly from it holding in type theory. This contrasts with the combinatorial construction in [Her15] where equations over face maps have to be proved by induction.

By taking the sum of each component of an indexed presentation over the indexing set of this component, one obtains back a presheaf in the ordinary sense that has a property of *Reedy fibrancy*, that is whose morphisms are projections in the set-theoretic sense. Such Reedy fibrant presheaves over a direct category have been studied in e.g. [Shu15], [KS17] and [ACK17, ACKS23], presenting generic constructions over such presheaves.

The indexed definition of a presheaf over a direct category is technically more involved than the presheaf definition, as it requires hard-wiring in the structure the dependencies between elements of the sets of the presheaf, including the coherence conditions between these dependencies, such as taking the *i*-th face of the *j*-th face of a *n*-simplex being the same as taking the (*j* − 1)-th face of the *i*-th face (when *j* > *i*). However, exhibiting a concrete instance of a presheaf in indexed form only requires providing the families, since the responsibility of defining maps and showing the coherence conditions is already accounted for in the definition of the structure.

## Reynolds parametricity and its unary and binary variants

In the context of functional programming, Reynolds parametricity [Rey83] interprets types as relations characterizing the observational behaviour of programs of this type. More generally, families over a product of sets, or *correspondences*, can be used in place of relations. Parametricity can then be iterated, and relying on the fibred presentation of correspondences as spans, it has been noted that iterated Reynolds parametricity has the structure of a cubical set [AK15, Mou16, JS17, Moe21, Moe22]. We obtain a *unary* variant of Reynolds *binary* parametricity by using predicates or families instead of relations or correspondences, and this is a form of realizability [BM12, Las14, Mou16]. Cubical set models which differ only by the arity one [BCM15] or two [BCH13a] were introduced, and this led to a general notion of affine *v*-ary cubes in [ND24]. In parallel, it has been noted that iterated unary parametricity has the structure of an augmented simplicial set<sup>e</sup>. This suggests that the definition of augmented semi-simplicial sets and semi-cubical sets can in turn be seen as particular instances of the restriction of Nuyts-Devriese's *v*-ary cubes to only faces, which we call *v*-sets, of presheaves over a *v*-semi-shape category made of words of some cardinal *v* + 1, where *v* = 1 gives augmented semi-simplicial sets and *v* = 2 gives semi-cubical sets.

<footnote><sup>b</sup> ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory</footnote>

<footnote><sup>c</sup>In hindsight, the title of the paper “A dependently-typed construction of semi-simplicial types” is somewhat confusing: it implicitly claimed to construct semi-simplicial types, but the construction was done in a type theory with Uniqueness of Identity Proofs. Consequently, what was really obtained was an indexed presentation of semi-simplicial sets. The confusion was however, common at the time.</footnote>

<footnote><sup>d</sup> github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/STypes.agda</footnote>

<footnote><sup>e</sup>Private communication with Hugo Moeneclaey and Thorsten Altenkirch.</footnote>
## II SEMI-SIMPLICIAL AND SEMI-CUBICAL SETS

In this section, we generalize semi-simplicial and semi-cubical sets to $\nu$-sets, subsuming the earlier definitions. We start with some introductory material on semi-simplicial and semi-cubical sets.

### Augmented semi-simplicial sets

Augmented semi-simplicial sets are defined similarly to semi-simplicial sets, except that the connected components are additionally dependent on a “color”. Conversely, semi-simplicial sets can be seen as augmented semi-simplicial sets over the singleton set of a fixed color. Let us associate dimension 0 to colors; then, points are dimension 1, lines are dimension 2, and so on. There is hence a shift by one when compared to semi-simplicial sets.

While ordinary semi-simplicial sets are presheaves over the semi-simplex category, augmented semi-simplicial sets are presheaves over $\Delta_+$. There are different ways to define $\Delta_+$, up to equivalence, and we use a definition that can be extended to semi-cubical sets in a straightforward manner.

II.0.1 Notation [Finite sequences] We denote finite sequences by $i_1...i_n$ for $i_j$ ranging over some domain. The empty sequence is written $\epsilon$.

II.0.2 Definition [$\Delta_+$] The definition of $\Delta_+$ is shown below. Note that, if $g \circ f$ is well-defined, then the length of $f$ is less than that of $g$. It can be shown that composition is associative and that id is neutral.

$$ \begin{array}{l} \text{Obj}_{\Delta_+} := \mathbb{N} \\ \text{Hom}_{\Delta_+}(p, n) := \{l \in \{0, \star\}^n \mid \text{number of } \star \text{ in } l = p\} \\ g \circ f := \begin{cases} f & \text{if } g = \epsilon \\ 0(g' \circ f) & \text{if } g = 0 g' \\ a(g' \circ f') & \text{if } g = \star g', f = a f', \text{ where } a = 0 \text{ or } \star \end{cases} \\ \text{id} := \star \dots \star n \text{ times for } \text{id} \in \text{Hom}_{\Delta_+}(n, n) \end{array} $$

II.0.3 Definition [Set$\Delta_+$] We define the category of augmented semi-simplicial sets as the functor category:

$$ \text{Set}_{\Delta_+} := \text{Set}^{\Delta_+^{\text{op}}} $$

To provide examples, we define the standard augmented $n$-semi-simplex.

II.0.4 Definition [$\Delta_+^n$] The standard augmented $n$-semi-simplex $\Delta_+^n$ is defined as the Yoneda embedding of $n \in \text{Obj}(\Delta_+)$:

$$ \begin{array}{l} \Delta_+^n : \text{Set}_{\Delta_+} \\ \Delta_+^n(p) := \text{Hom}(p, n) \\ \Delta_+^n(f) := \lambda g. g \circ f \end{array} $$

The standard augmented 0-semi-simplex is a singleton made of one color (in this case, black). Standard augmented $n$-semi-simplices for $n \ge 1$ have a geometric interpretation, and we illustrate them for dimensions 1, 2, and 3.

II.0.5 Example [$\Delta_+^1$] The standard augmented 1-semi-simplex can be pictured as a point, colored black, corresponding to the unique morphism in $\text{Hom}(0, 1)$. This point is the identity in $\text{Hom}(1, 1)$; it is hence shown as a singleton $\star$.

$\star$

II.0.6 Example [$\Delta_+^2$] The standard augmented 2-semi-simplex is drawn as two points, given by $\text{Hom}(1, 2)$, along with a line connecting them, given by $\text{Hom}(2, 2)$. We use black to denote the unique morphisms in $\text{Hom}(0, 1)$ and $\text{Hom}(0, 2)$.

$$ \star 0 \xrightarrow{\star\star} 0\star $$
## Contribution

The main contribution of the paper is to describe the details of a recipe that uniformly characterizes unary and binary iterated parametricity in indexed form, and to derive from it a new indexed presentation, called indexed v-sets, of augmented semi-simplicial and semi-cubical sets.

Our work is a step in the direction of the program initiated in [AK15] to develop parametricity-based models of parametric type theory [BCM15, NVD17, CH20] and cubical type theory [BCH13a, CCHM18, ABC$^+$21], which are closer to the syntax of type theory, and are likely to better reflect the definitional properties of type theory than presheaf-based cubical sets would. For example, consider the loss of definitional properties when interpreting “indexed” dependent types of type theory as “fibrations” in models such as locally cartesian closed categories [CGH14].

Our construction has the unique property of reflecting the structure of parametricity and of yielding both augmented semi-simplicial and semi-cubical sets from the same construction. The approach taken in [PL15] and [ACK16] takes benefit of the definitional compositionality of increasing injective maps, but we do not see how they could be generalized to yield semi-cubical sets.

Our mechanization can be found at github.com/artagnon/bonak. The construction was conceived in Summer 2019, and the mechanization began in late 2019. A sketch of the construction was presented at the 2020 HoTT-UF workshop, and the completion of the mechanization was reported at the TYPES 2022 conference.

# II SEMI-SIMPLICIAL AND SEMI-CUBICAL SETS

In this section, we generalize semi-simplicial and semi-cubical sets to v-sets, subsuming the earlier definitions. We start with some introductory material on semi-simplicial and semi-cubical sets.

## Augmented semi-simplicial sets

Augmented semi-simplicial sets are defined similarly to semi-simplicial sets, except that the connected components are additionally dependent on a “colour”. Conversely, semi-simplicial sets can be seen as augmented semi-simplicial sets over the singleton set of a fixed colour. Let us associate dimension $-1$ to colours; then, points are dimension $0$, lines are dimension $1$, and so on.

Ordinary semi-simplicial sets are presheaves over the semi-simplex category. Augmented semi-simplicial sets are presheaves over $\Delta_+$. There are different ways to define $\Delta_+$, up to equivalence, and we use a definition that can be extended to semi-cubical sets in a straightforward manner. In particular, we start numbering objects from $0$ instead of $-1$ so that there is a shift by one compared to the standard numbering of augmented semi-simplicial sets.

II.0.1 Notation [Finite sequences] We denote finite sequences by $i_1...i_n$ for $i_j$ ranging over some domain. The empty sequence is written $\epsilon$.

II.0.2 Definition [$\Delta_+$] The definition of $\Delta_+$ is shown below. Note that, if $g \circ f$ is well-defined, then the length of $f$ is less than or equal to that of $g$. It can be shown that composition is associative and that id is neutral.

$$ \mathrm{Obj}_{\Delta_+} := \mathbb{N} \\ \mathrm{Hom}_{\Delta_+}(p, n) := \{l \in \{0, \star\}^n \mid \text{number of } \star \text{ in } l = p\} $$

$$ g \circ f := \begin{cases} f & \text{if } g = \epsilon \\ 0 (g' \circ f) & \text{if } g = 0 g' \\ a (g' \circ f') & \text{if } g = \star g', f = a f', \text{ where } a = 0 \text{ or } \star \end{cases} $$

$$ \mathrm{id} := \star \dots \star n \text{ times for } \mathrm{id} \in \mathrm{Hom}_{\Delta_+}(n, n) $$

II.0.3 Definition [Set$\Delta_+$] We define the category of augmented semi-simplicial sets as the functor category:

$$ \mathrm{Set}_{\Delta_+} := \mathrm{Set}^{\Delta_+^{\mathrm{op}}} $$

To provide examples, we define the standard augmented $n$-semi-simplex, taking into account the shift by one in the numbering.
### II.0.7 Example $[\Delta_+^3] \Delta_+^3$ is drawn as three points, given by $\text{Hom}(1,3)$, three lines connecting them, given by $\text{Hom}(2,3)$, and a triangular filler given by $\text{Hom}(3,3)$.

<figure><img src="image_3.png" /></figure>

More generally, the standard augmented $(n+1)$-semi-simplex can be obtained by taking a copy of the standard augmented $n$-semi-simplex serving as a base, and gluing on top of it another copy lifted by one dimension. In the second copy, the color becomes an extra point, the points become lines connecting the points of the base to the extra point, and so on. In particular, the components of the base are those of the standard augmented $n$-semi-simplex postfixed by 0 while the components of the lifted copy are postfixed by $\star$. Note that the components may be oriented by letting each $n$-dimensional component point to the $(n-1)$-dimensional component obtained by replacing the leftmost $\star$ of the $n$-dimensional component with 0.

### Semi-cubical sets

Semi-cubical sets are defined like augmented semi-simplicial sets except that $\Delta_+$ is replaced by $\square$ in which we take sequences of $L, R$ and $\star$, instead of sequences of 0 and $\star$.

### II.0.8 Definition $[\square]$ The definition of $[\square]$ is shown below. The symbols $L$ and $R$ indicate opposite faces of a cube.

$$ \begin{array}{l} \text{Obj}_\square := \mathbb{N} \\ \text{Hom}_\square(p, n) := \{l \in \{L, R, \star\}^n \mid \text{number of } \star \text{ in } l = p\} \\ g \circ f := \begin{cases} f & \text{if } g = \epsilon \\ a(g' \circ f) & \text{if } g = a g', \text{ where } a = L \text{ or } R \\ a(g' \circ f') & \text{if } g = \star g', f = a f', \text{ where } a = L, R, \text{ or } \star \end{cases} \\ \text{id} := \star \dots \star n \text{ times} \end{array} $$

Again, if $g \circ f$ is well-defined, then the length of $f$ is less than that of $g$. It can be shown that composition is associative and that $\text{id}$ is neutral.

### II.0.9 Definition $[\text{Set}_\square]$ We define the category of semi-cubical sets as the functor category:

$$ \text{Set}_\square := \text{Set}^{\square\text{op}} $$

### II.0.10 Definition $[\square^n]$ The standard semi-cube $\square^n$ is defined as the Yoneda embedding of $n \in \text{Obj}(\square)$:

$$ \begin{array}{l} \square^n : \text{Set}_\square \\ \square^n(p) := \text{Hom}(p, n) \\ \square^n(f) := \lambda g \cdot g \circ f \end{array} $$

Standard $n$-semi-cubes have a geometric interpretation, which we illustrate for dimensions 0, 1, and 2.

### II.0.11 Example $[\square^0]$ $\square^0$ is $\text{Hom}(0,0)$, or the singleton set of the empty sequence:

$\epsilon$

### II.0.12 Example $[\square^1]$ $\square^1$ consists of two points, given by $\text{Hom}(0,1)$, and a line, given by $\text{Hom}(1,1)$.

$$ L \xrightarrow{\star} R $$

### II.0.13 Example $[\square^2]$ $\square^2$ consists of four points, given by $\text{Hom}(0,2)$, four lines connecting the four points, given by $\text{Hom}(1,2)$, and a filler, given by $\text{Hom}(2,2)$:

$$ \begin{array}{ccc} LR & \xrightarrow{\star R} & RR \\ L\star | & \star\star & | R\star \\ \hline LL & \xrightarrow{\star L} & RL \end{array} $$
II.0.4 Definition $[\Delta_+^n]$ The standard augmented $(n-1)$-semi-simplex $\Delta_+^{n-1}$ is defined as the Yoneda embedding of $n \in \text{Obj}(\Delta_+)$:

$$ \begin{align*} \Delta_+^{n-1} &::= \text{Set}_{\Delta_+} \\ \Delta_+^{n-1}(p) &::= \text{Hom}(p, n) \\ \Delta_+^{n-1}(f) &::= \lambda g \cdot g \circ f \end{align*} $$

The standard augmented $(-1)$-semi-simplex is a singleton made of one colour (in this case, black). Standard augmented $n$-semi-simplices for $n \ge 0$ have a geometric interpretation, and we illustrate them for dimensions 0, 1, and 2.

II.0.5 Example $[\Delta_+^0]$ The standard augmented 0-semi-simplex can be pictured as a point, coloured black, corresponding to the unique morphism in $\text{Hom}(0, 1)$. This point is the identity in $\text{Hom}(1, 1)$; it is hence shown as a singleton $\star$.

*

II.0.6 Example $[\Delta_+^1]$ The standard augmented 1-semi-simplex is drawn as two points, given by $\text{Hom}(1, 2)$, along with a line connecting them, given by $\text{Hom}(2, 2)$. We use black to denote the unique morphisms in $\text{Hom}(0, 1)$ and $\text{Hom}(0, 2)$.

$$ \star 0 \xrightarrow{**} 0 \star $$

II.0.7 Example $[\Delta_+^2]$ $\Delta_+^2$ is drawn as three points, given by $\text{Hom}(1, 3)$, three lines connecting them, given by $\text{Hom}(2, 3)$, and a triangular filler given by $\text{Hom}(3, 3)$.

<figure><img src="image_3.png" /></figure>

More generally, the standard augmented $(n+1)$-semi-simplex can be obtained by taking a copy of the standard augmented $n$-semi-simplex serving as a base, and gluing on top of it another copy lifted by one dimension. In the second copy, the colour becomes an extra point, the points become lines connecting the points of the base to the extra point, and so on. In particular, the components of the base are those of the standard augmented $n$-semi-simplex postfixed by 0 while the components of the lifted copy are postfixed by $\star$. Note that the components may be oriented by letting each $n$-dimensional component point to the $(n-1)$-dimensional component obtained by replacing the leftmost $\star$ of the $n$-dimensional component with 0.

## Semi-cubical sets

Semi-cubical sets are defined like augmented semi-simplicial sets except that $\Delta_+$ is replaced by $\square$ in which we take sequences of $L$, $R$ and $\star$, instead of sequences of 0 and $\star$.

II.0.8 Definition $[\square]$ The definition of $\square$ is shown below. The symbols $L$ and $R$ indicate opposite faces of a cube.

$$ \begin{align*} \text{Obj}_{\square} &::= \mathbb{N} \\ \text{Hom}_{\square}(p, n) &::= \{l \in \{L, R, \star\}^n \mid \text{number of } \star \text{ in } l = p\} \\ g \circ f &::= \begin{cases} f & \text{if } g = \epsilon \\ a (g' \circ f) & \text{if } g = a g', \text{ where } a = L \text{ or } R \\ a (g' \circ f') & \text{if } g = \star g', f = a f', \text{ where } a = L, R, \text{ or } \star \end{cases} \\ \text{id} &::= \star \dots \star n \text{ times} \end{align*} $$

Again, if $g \circ f$ is well-defined, then the length of $f$ is less than or equal to that of $g$. It can be shown that composition is associative and that $\text{id}$ is neutral.

II.0.9 Definition $[\text{Set}_{\square}]$ We define the category of semi-cubical sets as the functor category:

$$ \text{Set}_{\square} := \text{Set}^{\square \text{op}} $$
More generally, the standard $(n+1)$-semi-cube can be obtained by taking two copies of the standard $n$-semi-cube serving as bottom and top face and connecting them on their border by a cylinder obtained as a third copy stretched in the new dimension. The bottom and top faces are obtained from the standard $n$-semi-cube by postfixing with respectively $L$ and $R$ while the cylinder is obtained by postfixing with $\star$. Note that the components can be oriented by letting each $n$-dimensional component go from the $(n-1)$-dimensional component obtained by replacing the leftmost $\star$ with $L$, to the one obtained by replacing the leftmost $\star$ with $R$.

## $\nu$-sets

Let us call $\nu$-sets, the generalization of augmented semi-simplicial sets and semi-cubical sets obtained by building on an arbitrary alphabet $\nu$, so that the following holds:

<table><thead><tr><th>Cardinal of $\nu$</th><th>1</th><th>2</th></tr></thead><tbody><tr><td>Interpretation</td><td>Augmented semi-simplicial types</td><td>Semi-cubical types</td></tr></tbody></table>

To obtain this, we extend $\Delta_+$ and $\square$ in a straightforward manner into a category which we call $\mathcal{O}$.

II.0.14 Definition [○] The definition of $\nu$-semi-shape category is shown below. Note that, if $g \circ f$ is well-defined, then the length of $f$ is less than that of $g$. It can be shown that composition is associative and that id is neutral.

$$ \mathrm{Obj}_{\mathcal{O}} := \mathbb{N} \\ \mathrm{Hom}_{\mathcal{O}}(p, n) := \{l \in (\nu \sqcup \{\star\})^n \mid \text{number of } \star \text{ in } l = p\} $$

$$ g \circ f := \begin{cases} f & \text{if } g = \epsilon \\ a (g' \circ f) & \text{if } g = a g', \text{ where } a \in \nu \\ a (g' \circ f') & \text{if } g = \star g', f = a f', \text{ where } a \in \nu \text{ or } a = \star \end{cases} $$

$$ \mathrm{id} := \star \dots \star n \text{ times for } \mathrm{id} \in \mathrm{Hom}_{\mathcal{O}}(n, n) $$

A $\nu$-set is thus a contravariant functor $\phi$ from the $\nu$-semi-shape category to Set and we call $n$-$\nu$-semi-shape an element of $\phi(n)$. As in the augmented semi-simplicial and semi-cubical cases, the standard $(n+1)$-$\nu$-semi-shape is obtained by connecting together $\nu$ copies of the standard $n$-$\nu$-semi-shape with an extra copy stretched in the new dimension. We clarify in the next sections, how this process of construction is similar to the parametricity translation developed for functional programming [Rey83] and more generally for type theory [BJP10, BL11, AGJ14, BCM15].

# III TYPE THEORY

Martin-Löf's Type theory ([ML75, Mar84]) is a logical formalism based on the notion of a *type* rather than that of a *set*. It can be seen as a foundation of mathematics alternative to set theory and is the core of several tools for the formalization of mathematics such as Agda ([The23a]), Coq ([The23b]) and Lean ([dMKA+15]). In type theory, propositions are types and proofs are programs. Type theory includes *definitional equality*, by which all propositions and proofs are quotiented.

Type theory is a flexible formalism supporting different models. Some models are based on topological spaces, where equality is interpreted as path, and substitutivity of equality as transport [KL21]. These models support the univalence principle stating that equality of types mimics equivalence of types, leading to the development of Homotopy Type Theory [The13].

Types are organized in a hierarchy of universes written $\mathbf{Type}_m$ for $m$ a natural number. The main types in type theory are the type of dependent pairs, written $\Sigma a : A. B(a)$, the type of dependent functions, written $\Pi a : A. B(a)$, for $A$ a type and $B(a)$ a type dependent on the inhabitant $a$ of $A$, and the type of propositional equalities, written $t = u$. As a notation, the type of dependent pairs when $B$ is not dependent on $A$ is shortened into $A \times B$ and the type of dependent functions when $B$ is not dependent on $A$ is written $A \to B$. We assume our type theory to also include a distinguished singleton type, written unit, and with inhabitant $\star$, the type of boolean values, and the type of natural numbers. We also assume that our type theory includes the coinductive type of infinite dependent tuples. We write hd and tl the projections of dependent pairs, and refl for reflexivity. Logical propositions being types themselves, we use $\Pi$ to represent universal quantification and $\Sigma$ to represent existential quantification.

A type-theoretic notion of sets can be recovered in each universe as $\mathbf{HSet}_m$, denoting the subtype of $\mathbf{Type}_m$ for which paths are degenerated, using Uniqueness of Identity Proofs (UIP). Technically, this is expressed as a
II.0.10 Definition [□ⁿ] The standard semi-cube □ⁿ is defined as the Yoneda embedding of $n \in \text{Obj}(\Box)$:

$$ \Box^n : \text{Set}_\Box $$

$$ \Box^n(p) := \text{Hom}(p, n) $$

$$ \Box^n(f) := \lambda g. g \circ f $$

Standard *n*-semi-cubes have a geometric interpretation, which we illustrate for dimensions 0, 1, and 2.

II.0.11 Example [□⁰] □⁰ is Hom(0, 0), or the singleton set of the empty sequence:

$\epsilon$

II.0.12 Example [□¹] □¹ consists of two points, given by Hom(0, 1), and a line, given by Hom(1, 1).

$$ L \xrightarrow{\star} R $$

II.0.13 Example [□²] □² consists of four points, given by Hom(0, 2), four lines connecting the four points, given by Hom(1, 2), and a filler, given by Hom(2, 2):

$$ \begin{array}{ccc} LR & \xrightarrow{\star R} & RR \\ L\star | & \star\star & | R\star \\ LL & \xrightarrow{\star L} & RL \end{array} $$

More generally, the standard $(n+1)$-semi-cube can be obtained by taking two copies of the standard $n$-semi-cube serving as bottom and top face and connecting them on their border by a prism obtained as a third copy stretched in the new dimension. The bottom and top faces are obtained from the standard $n$-semi-cube by postfixing with respectively $L$ and $R$ while the prism is obtained by postfixing with $\star$. Note that the components can be oriented by letting each $n$-dimensional component go from the $(n-1)$-dimensional component obtained by replacing the leftmost $\star$ with $L$, to the one obtained by replacing the leftmost $\star$ with $R$.

## v-sets

Let us call $v$-sets, the generalization of augmented semi-simplicial sets and semi-cubical sets obtained by building on an arbitrary alphabet $v$, so that the following holds:

<table><tr><td>Cardinal of v</td><td>1</td><td>2</td></tr><tr><td>Interpretation</td><td>Augmented semi-simplicial sets</td><td>Semi-cubical sets</td></tr></table>

To obtain this, we extend $\Delta_+$ and □ in a straightforward manner into a category which we call $\mathcal{O}$.

II.0.14 Definition [○] The definition of $v$-semi-shape category is shown below. Note that, if $g \circ f$ is well-defined, then the length of $f$ is less than or equal to that of $g$. It can be shown that composition is associative and that id is neutral.

$$ \begin{align*} \text{Obj}_\mathcal{O} &:= \mathbb{N} \\ \text{Hom}_\mathcal{O}(p, n) &:= \{l \in (v \sqcup \{\star\})^n \mid \text{number of } \star \text{ in } l = p\} \\ g \circ f &:= \begin{cases} f & \text{if } g = \epsilon \\ a(g' \circ f) & \text{if } g = a g', \text{ where } a \in v \\ a(g' \circ f') & \text{if } g = \star g', f = a f', \text{ where } a \in v \text{ or } a = \star \end{cases} \\ \text{id} &:= \star \dots \star n \text{ times for } \text{id} \in \text{Hom}_\mathcal{O}(n, n) \end{align*} $$

A $v$-set is thus a contravariant functor $\phi$ from the $v$-semi-shape category to Set and we call $n$-$v$-semi-shape an element of $\phi(n)$. As in the augmented semi-simplicial and semi-cubical cases, the standard $(n+1)$-$v$-semi-shape is obtained by connecting together $v$ copies of the standard $n$-$v$-semi-shape with an extra copy stretched in the new dimension. We clarify in the next sections, how this process of construction is similar to the parametricity translation developed for functional programming [Rey83] and more generally for type theory [BJP10, BL11, AGJ14, BCM15].
structure equipping a domain Dom with the property `UIP`:

Dom : Type<sub>m</sub>

UIP : Πxy : Dom. Πpq : x = y. p = q

In `HSet<sub>m</sub>`, the following properties hold:

1. `UIP` holds on the unit type, `bool` type, as well as all types of finite cardinal $v$.

2. `UIP` propagates to $Σ$-types.

3. `UIP` propagates to $Π$-types, with some additional functional extensionality axioms.

By notation, `Type` and `HSet` mean `Type<sub>m</sub>` and `HSet<sub>m</sub>` at some unspecified universe level $m$.

We are also interested in extensional type theory, a type theory with the following reflection rule, where $=$ is propositional equality in some type and $≡$ is definitional equality [Mar84]:

$$ \frac{\Gamma \vdash p : t = u}{\Gamma \vdash t \equiv u} $$

Note that the reflection rule implies `UIP` so that `HSet` and `Type` are equivalent in extensional type theory. The reflection rules also implies functional extensionality. Extensional type theory is logically equivalent to intensional type theory extended with `UIP` and functional extensionality [Hof95].

# IV RELATING TO PARAMETRICITY

Recall from the introduction, the form taken by the indexed presentation of a semi-cubical set:

$$ \begin{array}{l@{\qquad}l} X_0 : & \texttt{HSet} \\ X_1 : & X_0 \times X_0 \to \texttt{HSet} \\ X_2 : \Pi abcd. & X_1(a, b) \times X_1(c, d) \times X_1(a, c) \times X_1(b, d) \to \texttt{HSet} \\ \dots & \end{array} $$

Here, the process of construction of the type of $X_1$ from that of $X_0$, and of the type of $X_2$ from that of $X_1$, is similar to iteratively applying a binary parametricity translation. The binary parametricity which we consider interprets a closed type $A$ by a family $A_*$ over $A \times A$, and this can be seen as a graph whose vertices are in $A$. Each type constructor is associated with the construction of a graph. To start with, the type of types `HSet` is interpreted as the family of type of families `HSet_*$`, which takes $A_L$ and $A_R$ in `HSet` and returns the type $A_L \times A_R \to \texttt{HSet}$ of families over $A_L$ and $A_R$. Also, for $A$ interpreted by $A_*$ and $B$ interpreted by $B_*$, a dependent function type $\Pi a : A.B$ is interpreted as the graph $(\Pi a : A.B)_*$ that takes two functions $f_L$ and $f_R$ of type $\Pi a : A.B$, and expresses that these functions map related arguments in $A$ to related arguments in $B$:

$$ (\Pi a : A.B)_*(f_L, f_R) \triangleq \Pi (a_L, a_R) : (A \times A). (A_*(a_L, a_R) \to B_*(f_L(a_L), f_R(a_R))) $$

Similarly, a product type $A \times B$ is interpreted as the graph $(A \times B)_*$ that relates two tuples $(a_L, b_L)$ and $(a_R, b_R)$ in $A \times B$ as follows:

$$ (A \times B)_*((a_L, b_L), (a_R, b_R)) \triangleq A_*(a_L, a_R) \times B_*(b_L, b_R) $$

In particular, for $X : \texttt{HSet}$, applying our parametricity translation is about associating to $X$ an inhabitant $X_*$ of $\texttt{HSet}_*(X, X)$ i.e. of $X \times X \to \texttt{HSet}$. In turn, applying the translation again to $X_* : X \times X \to \texttt{HSet}$ is about associating to $X_*$ an inhabitant $X_{**}$ of $(X \times X \to \texttt{HSet})_*(X_*, X_*)$ i.e. of:

$$ \Pi((x_{LL}, x_{LR}), (x_{RL}, x_{RR})) : ((X \times X) \times (X \times X)). (X_*(x_{LL}, x_{LR}) \times X_*(x_{RL}, x_{RR}) \to X_*(x_{LL}, x_{LR}) \times X_*(x_{LR}, x_{RR}) \to \texttt{HSet}) $$

which hints us at how the sequence $X_0, X_1, X_2$ can be seen as a sequence of inhabitants of the iteration of the composition of binary parametricity with the diagonal on types and type families, applied to an initial $X : \texttt{HSet}$:

$$ \begin{array}{l@{\qquad}l} X_0 & \triangleq X : & \texttt{HSet} \\ X_1 & \triangleq X_* : & \texttt{HSet}_*(X, X) \\ X_2 & \triangleq X_{**} : & (\texttt{HSet}_*(X, X))_*(X_*, X_*) \\ \dots & & \end{array} $$

This tells us how the informal type given to $X_2$ in the previous section could be rephrased so that it comes as the instance of a general recipe characterizing the type of all $X_i$.
# III TYPE THEORY

Martin-Löf's Type theory ([ML75, Mar84]) is a logical formalism based on the notion of a *type* rather than that of a *set*. It can be seen as a foundation of mathematics alternative to set theory and is the core of several tools for the formalization of mathematics such as Agda, Coq and Lean. In type theory, propositions are types and proofs are programs. Type theory includes *definitional equality*, by which all propositions and proofs are quotiented.

Type theory is a flexible formalism supporting different models. Some models come from homotopy theory, and are based on simplicial sets or related structures [HS94, KL21, BCH13b, CCHM15]: in these models, equality is interpreted as paths, and they support the univalence principle stating that equality of types mimics equivalence of types, leading to the development of Homotopy Type Theory [The13].

Types are organized in a hierarchy of universes written `Type<sub>m</sub>` for m a natural number. The main types in type theory are the type of dependent pairs, written Σ*a* : A. B(a), the type of dependent functions, written Π*a* : A. B(a), for A a type and B(a) a type dependent on the inhabitant *a* of A, and the type of propositional equalities, written *t* = *u*. As a notation, the type of dependent pairs when B is not dependent on A is shortened into A × B and the type of dependent functions when B is not dependent on A is written A → B. We assume our type theory to also include a distinguished singleton type, written `unit`, and with inhabitant `*`, the type of boolean values, and the type of natural numbers. We write `hd` and `tl` the projections of dependent pairs, and `refl` for reflexivity. Logical propositions being types themselves, we use Π to represent universal quantification and Σ to represent existential quantification. We also assume that our type theory includes a coinductively-defined notion of dependent streams described in the Appendix.

A type-theoretic notion of sets can be recovered in each universe as `HSet<sub>m</sub>`, denoting the subtype of `Type<sub>m</sub>` for which paths are degenerated, using Uniqueness of Identity Proofs (UIP). Technically, this is expressed as a structure equipping a domain `Dom` with the property `UIP`:

$$ \text{Dom} : \text{Type<sub>m</sub>} $$

$$ \text{UIP} : \Pi xy : \text{Dom}. \Pi pq : x = y. p = q $$

In `HSet<sub>m</sub>`, the following properties hold:

1. `UIP` holds on the `unit` type, `bool` type, as well as all types of finite cardinal $v$.

2. `UIP` propagates to Σ-types.

3. `UIP` propagates to Π-types, with some additional functional extensionality axioms.

By notation, `Type` and `HSet` mean `Type<sub>m</sub>` and `HSet<sub>m</sub>` at some unspecified universe level *m*.

We are also interested in *extensional type theory*, a type theory with the following reflection rule, where = is propositional equality in some type and ≡ is definitional equality [Mar84]:

$$ \Gamma \vdash p : t = u $$

$$ \Gamma \vdash t \equiv u $$

Note that the reflection rule implies `UIP` so that `HSet` and `Type` are equivalent in extensional type theory. The rule also implies functional extensionality. Extensional type theory is logically equivalent to intensional type theory extended with `UIP` and functional extensionality [Hof95].

# IV RELATING TO PARAMETRICITY

Recall from the introduction, the form taken by the indexed presentation of a semi-cubical set:

$$ X_0 : \text{HSet} $$

$$ X_1 : X_0 \times X_0 \to \text{HSet} $$

$$ X_2 : \Pi abcd. X_1(a, b) \times X_1(c, d) \times X_1(a, c) \times X_1(b, d) \to \text{HSet} $$

...

Here, the process of construction of the type of $X_1$ from that of $X_0$, and of the type of $X_2$ from that of $X_1$, is similar to iteratively applying a binary parametricity translation. The binary parametricity which we consider interprets a closed type $A$ by a family $A_*$ over $A \times A$, and this can be seen as a graph whose vertices are in $A$. Each type constructor is associated with the construction of a graph. To start with, the type of types `HSet` is interpreted as the family of type of families `HSet_*$`, which takes $A_L$ and $A_R$ in `HSet` and returns the type $A_L \times A_R \to \text{HSet}$ of families over $A_L$ and $A_R$. Also, for $A$ interpreted by $A_*$ and $B(a)$, for $a : A$, interpreted by $B_*( (a_L, a_R), a_*)$ with $a_* : A_*(a_L, a_R)$, a dependent function type $\Pi a : A. B(a)$ is interpreted as the graph
Notice, however, that the recipe obtained so far, $X_{n+1} : (S_n)_*(X_n, X_n)$ for $X_n : S_n$, applies parametricity on the syntax of the type of $X_n$. It does not directly yield a characterization of $S_n$ as a function from $n$. Reformulating the recipe as an explicit recursive construction, without requiring an interpretation of the syntax of types, is the main outcome of this work, together with the mechanization and the uniform treatment of augmented semi-simplicial and semi-cubical sets by means of the generalization to $\nu$-sets.

# V OUR CONSTRUCTION

In this section, we describe our parametricity-based construction of $\nu$-sets in indexed form at two levels of formality.

Sections V.1 and V.3 describe the construction at an informal level of discourse:

1. In V.1, we present it in informal extensional type theory where equational reasoning is left implicit, and we give an intuition for the construction in V.2.

2. While reasoning in extensional type theory is similar to reasoning in set theory regarding how equality is handled, extensional type theory has two limitations. The first limitation is that it enforces the principle of Uniqueness of Identity Proofs and this is inconsistent with the Univalence principle, thus making it inexpressible in Homotopy Type Theory. The second limitation is that we want the construction to be formalizable in the Coq proof assistant whose underlying type theory is intensional. Section V.3 thus rephrases the construction in (informal) intensional type theory.

Sections V.4, V.5, and V.6 describe additional issues to be addressed in order to get a fully formal construction:

1. The well-foundedness of the induction requires a special termination evidence which will be discussed in section V.4.

2. The construction is indexed over integers and holds under some constraints on the range of these integers. There is a standard formalization dilemma in this kind of situation: either the constraints on the range are embedded in the construction so that the construction makes sense only on the corresponding range, or the construction is made first on a more general domain than needed but restricted to a smaller domain at the time of use. We adopted the former approach, requiring the construction to be dependent on proofs of inequalities on natural numbers. We discuss how we deal with such dependencies in section V.5.

3. A number of standard groupoid properties of equality as well as type isomorphisms have been left implicit in the informal definition. This is discussed in section V.6.

## V.1 The construction in informal type theory

A $\nu$-set in indexed form is a sequence of families of $HSet$, that is $HSet_m$ for some universe level $m$. We call such sequence a $\nu$-set at level $m$, whose type thus lives in $HSet_{m+1}$.

Table 1 describes the type of a $\nu$-set at level $m$ in indexed form, as the type of a coinductively-defined infinite sequence of type families representing the limit of $n$-truncated $\nu$-sets: $\nu\text{Set}_m^{\ge n}$ denotes an infinite sequence $X_{n+1}, X_{n+2}, \dots$ dependent on a $n$-truncated $\nu$-set, $\nu\text{Set}_m^{\le n}$, so that, when $n$ is 0, it denotes a full $\nu$-set, written $\nu\text{Set}_m$. This is made possible because the 0-truncated $\nu$-set, $\nu\text{Set}_m^0$, is degenerated: it is an empty family, and there is thus only one 0-truncated $\nu$-set, namely the canonical inhabitant $\star$ of unit.

The definition of the type of a $n$-truncated $\nu$-set is in turn described in table 2. In the infinite sequence of type families representing a $\nu$-set, the $n$-th component is a type dependent over a *fullframe*. It is recursively defined in table 3, using the auxiliary definitions of *frame*, *layer* and *painting*. A *fullframe* describes a boundary of a standard form (simplex, cube), which we decompose into *layer*, and a *painting* corresponds to a filled frame. Notice that the type *layer* relies on an operator of frame restriction $\text{restr}_{\text{frame}}$ which is defined in table 4, and this restriction operator is in turn defined using auxiliary definitions $\text{restr}_{\text{layer}}$ and $\text{restr}_{\text{painting}}$.

Notably, the definition of $\text{restr}_{\text{layer}}$ relies on an equality expressing the commutation of the composition of two $\text{restr}_{\text{frame}}$. The proof of this commutation is worth being made explicit, which we do in table 5 using proof-term notations. The proof requires an induction on the dimension and on the structure of *frame*, *layer*, and *painting*. This is what $\text{coh}_{\text{frame}}$ does using auxiliary proofs $\text{coh}_{\text{layer}}$ and $\text{coh}_{\text{painting}}$. Even though it looks independent of the definitions from the other tables, $\text{coh}_{\text{frame}}$ has to be proved mutually with the definitions of *frame*, *layer*, *painting*, and their corresponding restrictions. More precisely, for a fixed $n$, the block of *frame*, $\text{restr}_{\text{frame}}$, and $\text{coh}_{\text{frame}}$ has to be defined in one go by induction on $p$. Also, each of *painting*, $\text{restr}_{\text{painting}}$, and $\text{coh}_{\text{painting}}$ is built by induction from $p$ to $n$. The *painting* block at $n$ relies on the *frame* block at $n$, but the converse dependency is only on lower $n$, so this is well-founded. Note that *layer*, $\text{restr}_{\text{layer}}$ and $\text{coh}_{\text{layer}}$ are just abbreviations. The exact way this mutual recursion is eventually formalized is explained in section V.4.

Note that for a fixed constant $n$, relying on the evaluation rules of type theory, the coherence conditions degenerate to a reflexivity proof, so that the construction builds an effective sequence of types not mentioning coherences anymore.
($Πa : A. B(a))_*$ that takes two functions $f_L$ and $f_R$ of type $Πa : A. B(a)$, and expresses that these functions map related arguments in A to related arguments in B:

$$ (\Pi a : A. B(a))_*(f_L, f_R) \triangleq \\ \Pi (a_L, a_R) : (A \times A). \Pi a_* : (A_*(a_L, a_R) B_*(a_L, a_R), a_*(f_L(a_L), f_R(a_R))) $$

Similarly, a product type $A \times B$ is interpreted as the graph $(A \times B)_*$ that relates two tuples $(a_L, b_L)$ and $(a_R, b_R)$ in $A \times B$ as follows:

$$ (A \times B)_*( (a_L, b_L), (a_R, b_R) ) \triangleq A_*(a_L, a_R) \times B_*(b_L, b_R) $$

In particular, for $X : HSet$, applying our parametricity translation is about associating to $X$ an inhabitant $X_*$ of $HSet_*(X, X)$ i.e. of $X \times X \to HSet$. In turn, applying the translation again to $X_* : X \times X \to HSet$ is about associating to $X_*$ an inhabitant $X_{**}$ of $(X \times X \to HSet)_*(X_*, X_*)$ i.e. of:

$$ \Pi((x_{LL}, x_{LR}), (x_{RL}, x_{RR})) : ((X \times X) \times (X \times X)). \\ (X_*(x_{LL}, x_{LR}) \times X_*(x_{RL}, x_{RR}) \to HSet) $$

which hints us at how the sequence $X_0, X_1, X_2$ can be seen as a sequence of inhabitants of the iteration of the composition of binary parametricity with the diagonal on types and type families, applied to an initial $X : HSet$:

$$ \begin{array}{lcl} X_0 & \triangleq & X \quad : \text{HSet} \\ X_1 & \triangleq & X_* \quad : \text{HSet}_*(X, X) \\ X_2 & \triangleq & X_{**} \quad : \text{(HSet}_*(X, X))_*(X_*, X_*) \\ \dots & & \end{array} $$

This tells us how the informal type given to $X_2$ in the previous section could be rephrased so that it comes as the instance of a general recipe characterizing the type of all $X_i$.

Notice, however, that the recipe obtained so far, $X_{n+1} : (S_n)_*(X_n, X_n)$ for $X_n : S_n$, applies parametricity on the syntax of the type of $X_n$. It does not directly yield a characterization of $S_n$ as a function from $n$. Reformulating the recipe as an explicit recursive construction, without requiring an interpretation of the syntax of types, is the main outcome of this work, together with the mechanization and the uniform treatment of augmented semi-simplicial and semi-cubical sets by means of the generalization to $v$-sets.

# V OUR CONSTRUCTION

In this section, we describe our parametricity-based construction of $v$-sets in indexed form at two levels of formality.

Sections V.1 and V.3 describe the construction at an informal level of discourse:

1. In V.1, we present it in informal extensional type theory where equational reasoning is left implicit, and we give an intuition for the construction in V.2.

2. While reasoning in extensional type theory is similar to reasoning in set theory regarding how equality is handled, extensional type theory has two limitations. The first limitation is that it enforces the principle of Uniqueness of Identity Proofs and this is inconsistent with the Univalence principle, thus making it inexpressible in Homotopy Type Theory. The second limitation is that we want the construction to be formalizable in the Coq proof assistant whose underlying type theory is intensional. Section V.3 thus rephrases the construction in (informal) intensional type theory. Since $v$-sets are 0-truncated types, we compensate for the absence of UIP by assuming a “local UIP”, requiring types to be HSet.

Sections V.4, V.5, and V.6 describe additional issues to be addressed in order to get a fully formal construction:

1. The well-foundedness of the induction requires a special termination evidence which will be discussed in section V.4.

2. The construction is indexed over integers and holds under some constraints on the range of these integers. There is a standard formalization dilemma in this kind of situation: either the constraints on the range are embedded in the construction so that the construction makes sense only on the corresponding range, or the construction is made first on a more general domain than needed but restricted to a smaller domain at the time of use. We adopted the former approach, requiring the construction to be dependent on proofs of inequalities on natural numbers. We discuss how we deal with such dependencies in section V.5.

3. A number of standard groupoid properties of equality as well as type isomorphisms have been left implicit in the informal definition. This is discussed in section V.6.
<table><caption>Table 1: Main definition</caption><tr><td>νSet<sub>m</sub></td><td>:</td><td>HSet<sub>m+1</sub></td></tr><tr><td>νSet<sub>m</sub></td><td>Δ</td><td>νSet<sub>m</sub><sup>≥0</sup>(*)</td></tr><tr><td>νSet<sub>m</sub><sup>≥n</sup></td><td>(D : νSet<sub>m</sub><sup>≤n</sup>)</td><td>HSet<sub>m+1</sub></td></tr><tr><td>νSet<sub>m</sub><sup>≥n</sup></td><td>D</td><td>ΣR : νSet<sub>m</sub><sup>=n</sup>(D), νSet<sub>m</sub><sup>≥n+1</sup>(D, R)</td></tr></table>

<table><caption>Table 2: Truncated $ν$-sets, the core</caption><tr><td>νSet<sub>m</sub><sup>≤n</sup></td><td>:</td><td>HSet<sub>m+1</sub></td></tr><tr><td>νSet<sub>m</sub><sup>≤0</sup></td><td>Δ</td><td>unit</td></tr><tr><td>νSet<sub>m</sub><sup>≤n'+1</sup></td><td>Δ</td><td>ΣD : νSet<sub>m</sub><sup>≤n'</sup>, νSet<sub>m</sub><sup>=n'</sup>(D)</td></tr><tr><td>νSet<sub>m</sub><sup>=n</sup></td><td>(D : νSet<sub>m</sub><sup>≤n</sup>)</td><td>HSet<sub>m</sub></td></tr><tr><td>νSet<sub>m</sub><sup>=n</sup></td><td>D</td><td>fullframe<sub>m</sub><sup>n</sup>(D) → HSet<sub>m</sub></td></tr></table>

<table><caption>Table 3: frame, layer, and painting</caption><tr><td>fullframe<sup>n</sup></td><td>(D : νSet<sub>m</sub><sup>≤n</sup>)</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>fullframe<sup>n</sup></td><td>D</td><td>Δ</td><td>frame<sup>n,n</sup>(D)</td></tr><tr><td>frame<sup>n,p,p≤n</sup></td><td>(D : νSet<sub>m</sub><sup>≤n</sup>)</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>frame<sup>n,0</sup></td><td>D</td><td>Δ</td><td>unit</td></tr><tr><td>frame<sup>n,p'+1</sup></td><td>D</td><td>Δ</td><td>Σd : frame<sup>n,p'</sup>(D), layer<sup>n,p'</sup>(d)</td></tr><tr><td>layer<sup>n,p,p&lt;n</sup></td><td>{D : νSet<sub>m</sub><sup>≤n</sup>}<br>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>layer<sup>n,p</sup></td><td>D d</td><td>Δ</td><td>Πωadem<br>painting<sup>n-1,p</sup>(D.2)(restr<sub>frame,ω,p</sub>(d))</td></tr><tr><td>painting<sup>n,p,p≤n</sup></td><td>(D : νSet<sub>m</sub><sup>≤n</sup>)<br>(E : νSet<sub>m</sub><sup>=n</sup>(D))<br>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>painting<sup>n,p,p=n</sup></td><td>D E d</td><td>Δ</td><td>E(d)</td></tr><tr><td>painting<sup>n,p,p&lt;n</sup></td><td>D E d</td><td>Δ</td><td>Σl : layer<sup>n,p</sup>(d), painting<sup>n,p+1</sup>(E)(d, l)</td></tr></table>

<table><caption>Table 4: q-th projection of restr, or faces</caption><tr><td>restr<sup>n,p,p≤q≤n-1</sup><sub>frame,ε,q</sub></td><td>{D : νSet<sup>≤n</sup>}<br>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>frame<sup>n-1,p</sup>(D.1)</td></tr><tr><td>restr<sup>n,0</sup><sub>frame,ε,q</sub></td><td>D *</td><td>Δ</td><td>*</td></tr><tr><td>restr<sup>n,p'+1</sup><sub>frame,ε,q</sub></td><td>D (d, l)</td><td>Δ</td><td>(restr<sup>n,p'</sup><sub>frame,ε,q</sub>(d), restr<sup>n,p'</sup><sub>layer,ε,q-1</sub>(l))</td></tr><tr><td>restr<sup>n,p,p≤q≤n-2</sup><sub>layer,ε,q</sub></td><td>{D : νSet<sup>≤n</sup>}<br>{d : frame<sup>n,p</sup>(D)}<br>(l : layer<sup>n,p</sup>(d))</td><td>:</td><td>layer<sup>n-1,p</sup>(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>restr<sup>n,p</sup><sub>layer,ε,q</sub></td><td>D d l</td><td>Δ</td><td>λω.(restr<sup>n-1,p</sup><sub>painting,ε,q</sub>(D.2)(l<sub>ω</sub>))</td></tr><tr><td>restr<sup>n,p,p≤q≤n-1</sup><sub>painting,ε,q</sub></td><td>(D : νSet<sup>≤n</sup>)<br>(E : νSet<sup>=n</sup>(D))<br>(d : frame<sup>n,p</sup>(D))<br>(c : painting<sup>n,p</sup>(E)(d))</td><td>:</td><td>painting<sup>n-1,p</sup>(D.2)(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>restr<sup>n,p,p=q</sup><sub>painting,ε,q</sub></td><td>D E d (l, _)</td><td>Δ</td><td>l<sub>ε</sub></td></tr><tr><td>restr<sup>n,p,p<≤q</sup><sub>painting,ε,q</sub></td><td>D E d (l, c)</td><td>Δ</td><td>(restr<sup>n,p</sup><sub>layer,ε,q</sub>(l), restr<sup>n,p+1</sup><sub>painting,ε,q</sub>(E)(c))</td></tr></table>

<table><caption>Table 5: Commutation of q-th projection and r-th projection, or coherence conditions</caption><tr><td>coh<sup>n,p,p≤r≤q≤n-2</sup><sub>frame,ε,ω,q,r</sub></td><td>{D : νSet<sup>≤n</sup>}<br>(d : frame(D))</td><td>:</td><td>restr<sup>n-1,p</sup><sub>frame,ε,q</sub>(restr<sup>n,p</sup><sub>frame,ω,r</sub>(d))<br>= restr<sup>n-1,p</sup><sub>frame,ω,r</sub>(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>coh<sup>n,0</sup><sub>frame,ε,ω,q,r</sub></td><td>D *</td><td>Δ</td><td>refl(*)</td></tr><tr><td>coh<sup>n,p'+1</sup><sub>frame,ε,ω,q,r</sub></td><td>D (d, l)</td><td>Δ</td><td>(coh<sup>n,p'</sup><sub>frame,ε,ω,q,r</sub>(d), coh<sup>n,p'</sup><sub>layer,ε,ω,q,r</sub>(l))</td></tr><tr><td>coh<sup>n,p,p<≤r</sup><sub>layer,ε,ω,q,r</sub></td><td>(D : νSet<sup>≤n</sup>)<br>{d : frame(D)}<br>(l : layer(d))</td><td>:</td><td>restr<sup>n-1,p</sup><sub>layer,ε,q</sub>(restr<sup>n,p</sup><sub>layer,ω,r</sub>(l))<br>= restr<sup>n-1,p</sup><sub>layer,ω,r</sub>(restr<sup>n,p</sup><sub>layer,ε,q+1</sub>(l))</td></tr><tr><td>coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub></td><td>D d l</td><td>Δ</td><td>λθ. coh<sup>n-1,p</sup><sub>painting,ε,ω,q-1,r-1</sub>(D.2)(l<sub>θ</sub>)</td></tr><tr><td>coh<sup>n,p,p≤r</sup><sub>painting,ε,ω,q,r</sub></td><td>(E : νSet<sup>=n</sup>(D))<br>(d : frame(D))<br>(c : painting(E)(d))</td><td>:</td><td>restr<sup>n-1,p</sup><sub>painting,ε,q</sub>(D.2)(restr<sup>n,p</sup><sub>painting,ω,r</sub>(E)(c))<br>= restr<sup>n-1,p</sup><sub>painting,ω,r</sub>(D.2)(restr<sup>n,p</sup><sub>painting,ε,q+1</sub>(E)(c))</td></tr><tr><td>coh<sup>n,p,p=r</sup><sub>painting,ε,ω,q,r</sub></td><td>D E d (l, _)</td><td>Δ</td><td>refl(restr<sup>n-1,p</sup><sub>painting,ε,q-1</sub>(D.2)(l<sub>ε</sub>))</td></tr><tr><td>coh<sup>n,p,p<≤r</sup><sub>painting,ε,ω,q,r</sub></td><td>D E d (l, c)</td><td>Δ</td><td>(coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub>(l), coh<sup>n,p+1</sup><sub>painting,ε,ω,q,r</sub>(E)(c))</td></tr></table>
## V.1 The construction in informal type theory

A $v$-set in indexed form is a sequence of families of $HSet$, that is $HSet_m$ for some universe level $m$. We call such sequence a $v$-set at level $m$, whose type thus lives in $HSet_{m+1}$.

Table 1 describes the type of a $v$-set at level $m$ as a dependent stream of type families representing the limit of $n$-truncated $v$-sets. Using the notations of Section III and of the Appendix, the recursive equation $vSet_m^{\ge n} D \triangleq \Sigma R : vSet_m^{=n}(D) \cdot vSet_m^{\ge n+1}(D, R)$ from the table formally corresponds to the dependent stream given by $Stream_{\Sigma n. vSet_m^{< n}, \lambda(n, D) \cdot vSet_m^{=n}(D), \lambda((n, D), R) \cdot (n+1, (D, R))}(n, D)$. Therefore, $vSet_m^{\ge n}$ denotes an infinite sequence $X_n, X_{n+1}, \dots$ dependent on a ($< n$)-truncated $v$-set, $vSet_m^{< n}$, so that, when $n$ is 0, it denotes a full $v$-set, written $vSet_m$. This is made possible because the ($< 0$)-truncated $v$-set, $vSet_m^{< 0}$, is degenerated: it is an empty family, and there is thus only one ($< 0$)-truncated $v$-set, namely the canonical inhabitant $\star$ of unit.

The definition of the type of a $n$-truncated $v$-set is in turn described in table 2. In the infinite sequence of type families representing a $v$-set, the $n$-th component is a type dependent over a **fullframe**. It is recursively defined in table 3, using the auxiliary definitions of **frame**, **layer** and **painting**. A **fullframe** describes a boundary of a standard form (simplex, cube), which we decompose into **layer**, and a **painting** corresponds to a filled frame. Notice that the type **layer** relies on an operator of frame restriction $restr_{frame}$ which is defined in table 4, and this restriction operator is in turn defined using auxiliary definitions $restr_{layer}$ and $restr_{painting}$.

<table><caption>**Table 1:** Main definition</caption><tr><td>vSet<sub>m</sub></td><td>:</td><td>HSet<sub>m+1</sub></td></tr><tr><td>vSet<sub>m</sub></td><td>△</td><td>vSet<sub>m</sub><sup>≥0</sup> (*)</td></tr><tr><td>vSet<sub>m</sub><sup>≥n</sup></td><td>(D : vSet<sub>m</sub><sup>&lt;n</sup>)</td><td>HSet<sub>m+1</sub></td></tr><tr><td>vSet<sub>m</sub><sup>≥n</sup></td><td>D</td><td>ΣR : vSet<sub>m</sub><sup>=n</sup>(D) . vSet<sub>m</sub><sup>&ge; n+1</sup>(D, R)</td></tr></table>

<table><caption>**Table 2:** Truncated $v$-sets, the core</caption><tr><td>vSet<sub>m</sub><sup>&lt;n</sup></td><td>:</td><td>HSet<sub>m+1</sub></td></tr><tr><td>vSet<sub>m</sub><sup>≤0</sup></td><td>△</td><td>unit</td></tr><tr><td>vSet<sub>m</sub><sup>≤ n'+1</sup></td><td>△</td><td>ΣD : vSet<sub>m</sub><sup>&lt;n'</sup> . vSet<sub>m</sub><sup>=n'</sup>(D)</td></tr><tr><td>vSet<sub>m</sub><sup>=n</sup></td><td>(D : vSet<sub>m</sub><sup>&lt;n</sup>)</td><td>HSet<sub>m+1</sub></td></tr><tr><td>vSet<sub>m</sub><sup>=n</sup></td><td>D</td><td>fullframe<sub>m</sub><sup>n</sup>(D) → HSet<sub>m</sub></td></tr></table>

<table><caption>**Table 3:** frame, layer, and painting</caption><tr><td>fullframe<sup>n</sup></td><td>(D : vSet<sub>m</sub><sup>&lt;n</sup>)</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>fullframe<sup>n</sup></td><td>D</td><td>△</td><td>frame<sup>n,n</sup>(D)</td></tr><tr><td>frame<sup>n,p,p≤n</sup></td><td>(D : vSet<sub>m</sub><sup>&lt;n</sup>)</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>frame<sup>n,0</sup></td><td>D</td><td>△</td><td>unit</td></tr><tr><td>frame<sup>n,p'+1</sup></td><td>D</td><td>△</td><td>Σd : frame<sup>n,p'</sup>(D) . layer<sup>n,p'</sup>(d)</td></tr><tr><td>layer<sup>n,p,p&lt;n</sup></td><td>{D : vSet<sub>m</sub><sup>&lt;n</sup>}<br>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>layer<sup>n,p</sup></td><td>D d</td><td>△</td><td>Πω<sub>.</sub>painting<sup>n-1,p</sup>(D.2)(restr<sup>n,p</sup><sub>frame,ω,p</sub>(d))</td></tr><tr><td>painting<sup>n,p,p≤n</sup></td><td>(E : vSet<sub>m</sub><sup>=n</sup>(D))<br>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>HSet<sub>m</sub></td></tr><tr><td>painting<sup>n,p,p=n</sup></td><td>D E d</td><td>△</td><td>E(d)</td></tr><tr><td>painting<sup>n,p,p&lt;n</sup></td><td>D E d</td><td>△</td><td>Σl : layer<sup>n,p</sup>(d) . painting<sup>n,p+1</sup>(E)(d, l)</td></tr></table>

Notably, the definition of $restr_{layer}$ relies on an equality expressing the commutation of the composition of two $restr_{frame}$. The proof of this commutation is worth being made explicit, which we do in table 5 using proof-term notations. The proof requires an induction on the dimension and on the structure of *frame*, *layer*, and *painting*. This is what $coh'_{frame}$ does using auxiliary proofs $coh'_{layer}$ and $coh'_{painting}$. Even though it looks independent of the definitions from the other tables, $coh'_{frame}$ has to be proved mutually with the definitions of *frame*, *layer*, *painting*, and their corresponding restrictions. More precisely, for a fixed $n$, the block of *frame*, $restr_{frame}$, and $coh'_{frame}$ has to be defined in one go by induction on $p$. Also, each of *painting*, $restr_{painting}$, and
## V.2 Intuition for our formal construction

There is a fullframe for each dimension $n$, written fullframe$^n$, and every $X_n$ is uniformly assigned a type of the form fullframe$^n \to HSet. Here, fullframe$^n$ is a “telescope” collecting all arguments of the type of $X_i$ in section IV as a nesting of $\Sigma$-types.

To illustrate how to recursively build fullframe$^n$, let us begin by setting fullframe$^0 \triangleq \text{unit}$, so that the type HSet given to $X_0$ in section IV can be equivalently formulated as unit $\to$ HSet. Then, more generally, let each fullframe$^n$ consist of $n$ layers, written layer$^{n,p}$ with $p < n$, that we stack in order, starting from unit, and writing frame$^{n,p}$ for the $p$ first layers of a fullframe$^n$, so that fullframe$^n$ is frame$^{n,n}$. For instance, $X_1$ is made of one layer, so that it can be written as a $\Sigma$-type of an inhabitant of unit and layer$^{1,0}$. Then, $X_2$ is similarly made of two layers.

<figure><img src="image_4.png" /></figure>

Let us now illustrate the construction of fullframe$^3$, necessary to build the type of $X_3$.

<figure><img src="image_5.png" /></figure>

The figure on the left is frame$^{3,1}$, in the middle is frame$^{3,2}$, and on the right is frame$^{3,3}$, which is full. Further, frame$^{3,1}$ is made of one layer, layer$^{3,0}$, shown in blue, frame$^{3,2}$ is made of one additional layer, layer$^{3,1}$, shown in red, frame$^{3,3}$ is made of one more layer, layer$^{3,2}$, shown in green.

We illustrated here the cubical case, that is $\nu = 2$, but, in general, a layer$^{n,p}$ is a product of $\nu$ painting$^{n-1,p}$. A painting$^{n,0}$ is a $n$-dimensional object corresponding to a filled fullframe$^n$. More generally, a painting$^{n,p}$ is an $n$-dimensional object which has the form of a painting$^{n-p,0}$, thus of $(n-p)$-dimensional form, but shifted and living in dimensions $p$ to $n$. Such painting$^{n,p}$ fills a space framed by a partial frame$^{n,p}$ so that, together, they
<table><caption>**Table 4:** q-th projection of restr, or faces</caption><tbody><tr><td>restr<sup>n,p</sup><sub>frame,ε,q</sub></td><td>{D : vSet<sup>n</sup>}<br/>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>frame<sup>n-1,p</sup>(D.1)</td></tr><tr><td>restr<sup>n,0</sup><sub>frame,ε,q</sub></td><td>D *</td><td>△</td><td>*</td></tr><tr><td>restr<sup>n,p'+1</sup><sub>frame,ε,q</sub></td><td>D (d, l)</td><td>△</td><td>(restr<sup>n,p'</sup><sub>frame,ε,q</sub>(d), restr<sup>n,p'</sup><sub>layer,ε,q-1</sub>(l))</td></tr><tr><td>restr<sup>n,p</sup><sub>layer,ε,q</sub></td><td>{D : vSet<sup>n</sup>}<br/>{d : frame<sup>n,p</sup>(D)}<br/>(l : layer<sup>n,p</sup>(d))</td><td>:</td><td>layer<sup>n-1,p</sup>(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>restr<sup>n,p</sup><sub>layer,ε,q</sub></td><td>D d l</td><td>△</td><td>λω.(restr<sup>n-1,p</sup><sub>painting,ε,q</sub>(D.2)(l<sub>ω</sub>))</td></tr><tr><td>restr<sup>n,p</sup><sub>painting,ε,q</sub></td><td>(D : vSet<sup>n</sup>)<br/>(E : vSet<sup>=n</sup>(D))<br/>(d : frame<sup>n,p</sup>(D))<br/>(c : painting<sup>n,p</sup>(E)(d))</td><td>:</td><td>painting<sup>n-1,p</sup>(D.2)(restr<sup>n,p</sup><sub>frame,ε,q</sub>(d))</td></tr><tr><td>restr<sup>n,p</sup><sub>painting,ε,q</sub></td><td>D E d (l, -)</td><td>△</td><td>l<sub>ε</sub></td></tr><tr><td>restr<sup>n,p</sup><sub>painting,ε,q</sub></td><td>D E d (l, c)</td><td>△</td><td>(restr<sup>n,p</sup><sub>layer,ε,q-1</sub>(l), restr<sup>n,p+1</sup><sub>painting,ε,q</sub>(E)(c))</td></tr></tbody></table>

<table><caption>**Table 5:** Commutation of q-th projection and r-th projection, or coherence conditions</caption><tbody><tr><td>coh<sup>n,p</sup><sub>frame,ε,ω,q,r</sub></td><td>{D : vSet<sup>n</sup>}<br/>(d : frame(D))</td><td>:</td><td>restr<sup>n-1,p</sup><sub>frame,ε,q</sub>(restr<sup>n,p</sup><sub>frame,ω,r</sub>(d))<br/>= restr<sup>n-1,p</sup><sub>frame,ω,r</sub>(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>coh<sup>n,0</sup><sub>frame,ε,ω,q,r</sub></td><td>D *</td><td>△</td><td>refl(*)</td></tr><tr><td>coh<sup>n,p'+1</sup><sub>frame,ε,ω,q,r</sub></td><td>D (d, l)</td><td>△</td><td>(coh<sup>n,p'</sup><sub>frame,ε,ω,q,r</sub>(d), coh<sup>n,p'</sup><sub>layer,ε,ω,q-1,r-1</sub>(l))</td></tr><tr><td>coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub></td><td>{D : vSet<sup>n</sup>}<br/>{d : frame(D)}<br/>(l : layer(d))</td><td>:</td><td>restr<sup>n-1,p</sup><sub>layer,ε,q</sub>(restr<sup>n,p</sup><sub>layer,ω,r</sub>(l))<br/>= restr<sup>n-1,p</sup><sub>layer,ω,r</sub>(restr<sup>n,p</sup><sub>layer,ε,q+1</sub>(l))</td></tr><tr><td>coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub></td><td>D d l</td><td>△</td><td>λθ. coh<sup>n-1,p</sup><sub>painting,ε,ω,q,r</sub>(D.2)(l<sub>θ</sub>)</td></tr><tr><td>coh<sup>n,p</sup><sub>painting,ε,ω,q,r</sub></td><td>{D : vSet<sup>n</sup>}<br/>(E : vSet<sup>=n</sup>(D))<br/>{d : frame(D)}<br/>(c : painting(E)(d))</td><td>:</td><td>restr<sup>n-1,p</sup><sub>painting,ε,q</sub>(D.2)(restr<sup>n,p</sup><sub>painting,ω,r</sub>(E)(c))<br/>= restr<sup>n-1,p</sup><sub>painting,ω,r</sub>(D.2)(restr<sup>n,p</sup><sub>painting,ε,q+1</sub>(E)(c))</td></tr><tr><td>coh<sup>n,p</sup><sub>painting,ε,ω,q,r</sub></td><td>D E d (l, -)</td><td>△</td><td>refl(restr<sup>n-1,p</sup><sub>painting,ε,q-1</sub>(D.2)(l<sub>ε</sub>))</td></tr><tr><td>coh<sup>n,p</sup><sub>painting,ε,ω,q,r</sub></td><td>D E d (l, c)</td><td>△</td><td>(coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub>(l), coh<sup>n,p+1</sup><sub>painting,ε,ω,q,r</sub>(E)(c))</td></tr></tbody></table>

coh' is built by induction from *p* to *n*. The *painting* block at *n* relies on the *frame* block at *n*, but the converse dependency is only on lower *n*, so this is well-founded. Note that *layer*, *restr*<sub>layer</sub> and *coh*'<sub>layer</sub> are just abbreviations. The exact way this mutual recursion is eventually formalized is explained in section V.4.

Note that for a fixed constant *n*, relying on the evaluation rules of type theory, the coherence conditions degenerate to a reflexivity proof, so that the construction builds an effective sequence of types not mentioning coherences anymore.

## V.2 Intuition for our formal construction

There is a *fullframe* for each dimension *n*, written *fullframe*<sup>*n*</sup>, and every $X_n$ is uniformly assigned a type of the form *fullframe*<sup>*n*</sup> → *HSet*. Here, *fullframe*<sup>*n*</sup> is a “telescope” collecting all arguments of the type of $X_n$ in section IV as a nesting of Σ-types.

To illustrate how to recursively build *fullframe*<sup>*n*</sup>, let us begin by setting *fullframe*<sup>0</sup> △= unit, so that the type *HSet* given to $X_0$ in section IV can be equivalently formulated as unit → *HSet*. Then, more generally, let each *fullframe*<sup>*n*</sup> consist of *n* layers, written *layer*<sup>*n*,p</sup> with *p* < *n*, that we stack in order, starting from unit, and writing *frame*<sup>*n*,p</sup> for the *p* first layers of a *fullframe*<sup>*n*</sup>, so that *fullframe*<sup>*n*</sup> is *frame*<sup>*n*,n</sup>. For instance, $X_1$ is made of one layer, so that it can be written as a Σ-type of an inhabitant of unit and *layer*<sup>1,0</sup>. Then, $X_2$ is similarly made of two layers.
<figure><img src="image_4.png" /></figure>

Let us now illustrate the construction of fullframe³, necessary to build the type of X₃.

<figure><img src="image_5.png" /></figure>

The figure on the left is frame<sup>3,1</sup>, in the middle is frame<sup>3,2</sup>, and on the right is frame<sup>3,3</sup>, which is full. Further, frame<sup>3,1</sup> is made of one layer, layer<sup>3,0</sup>, shown as the front and back faces (blue boxes), frame<sup>3,2</sup> is made of one additional layer, layer<sup>3,1</sup>, shown as the left and right faces (red boxes), frame<sup>3,3</sup> is made of one more layer, layer<sup>3,2</sup>, shown as the top face (green box).

We illustrated here the cubical case, that is $v = 2$, but, in general, a *layer*<sup>*n*,p</sup> is a product of $v$ *painting*<sup>*n*−1,*p*</sup>. A *painting*<sup>*n*,0</sup> is a *n*-dimensional object corresponding to a filled *fullframe*<sup>*n*</sup>. More generally, a *painting*<sup>*n*,p</sup> is an *n*-dimensional object which has the form of a *painting*<sup>*n*−*p*,*0</sup>, thus of (*n* − *p*)-dimensional form, but shifted and living in dimensions *p* to *n*. Such *painting*<sup>*n*,p</sup> fills a space framed by a partial *frame*<sup>*n*,p</sup> so that, together, they form a filled *fullframe*<sup>*n*</sup>. For instance, in the picture, each of the two *painting*<sup>2,0</sup> of *layer*<sup>3,0</sup> is a filled blue square, each of the two *painting*<sup>2,1</sup> of *layer*<sup>3,1</sup> is a line, shown as lines across the left and right faces (red lines), stretched into a partial square filling the partial frames made of respectively, the left and right border of the front-back faces (blue), and each of the two *painting*<sup>2,2</sup> of *layer*<sup>3,2</sup> is the point shown on the top face (green point), stretched into a partial square filling the full frames made respectively of the upper and lower borders of the front-back and left-right faces (blue and red squares). A *painting*<sup>*n*,p</sup> complements a *frame*<sup>*n*,p</sup> by adding layers needed to form a *fullframe*<sup>*n*</sup> and by filling the resulting *fullframe*<sup>*n*</sup> with an inhabitant of $X_n$. Layers are added from dimension *n* to dimension *p*, opposite to the order from 0 to *p* the *frame*<sup>*n*,p</sup> are built, as shown below.

$$ frame^{n,p} \triangleq \Sigma a_n : (\dots (\Sigma * : \text{unit. } layer^{n,0}) \dots). layer^{n,p-1} $$

$$ painting^{n,p} \triangleq \Sigma l_p : layer^{n,p}. (\dots (\Sigma l_n : layer^{n,n-1} \cdot X_n) \dots) $$
## V.3 From extensional to intensional type theory

In this section, we intend to get rid of the reflection rule and make explicit the equational reasoning step needed to rephrase the construction in intensional type theory. For readability purposes, we make only explicit in this section the key coherence conditions of the construction. Other cases of equality reasoning would have to be made explicit to fully obtain a construction in intensional type theory, but these steps are standard enough to be omitted at this stage. See section V.6 for the details.

The need for transport along a proof of commutation of $restr_{frame}$ in the definition of $restr_{layer}$ is made explicit in table 4', where the arrow over $coh_{frame}$ indicates the direction of rewrite.

<table><caption>Table 4': q-th projection of $restr$, or faces</caption><tbody><tr><td>restr<sup>n,p,p≤q≤n-1</sup><sub>frame,ε,q</sub></td><td>{D : νSet<sup>n</sup>}<br/>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>frame<sup>n-1,p</sup>(D.1)</td></tr><tr><td>restr<sup>n,0</sup><sub>frame,ε,q</sub></td><td>D *</td><td>Δ</td><td>*</td></tr><tr><td>restr<sup>n,p'+1</sup><sub>frame,ε,q</sub></td><td>D (d, l)</td><td>Δ</td><td>(restr<sup>n,p'</sup><sub>frame,ε,q</sub>(d), restr<sup>n,p'</sup><sub>layer,ε,q-1</sub>(l))</td></tr><tr><td>restr<sup>n,p,p≤q≤n-2</sup><sub>layer,ε,q</sub></td><td>{D : νSet<sup>n</sup>}<br/>{d : frame<sup>n,p</sup>(D)}<br/>(l : layer<sup>n,p</sup>(d))</td><td>:</td><td>layer<sup>n-1,p</sup>(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>restr<sup>n,p</sup><sub>layer,ε,q</sub></td><td>D d l</td><td>Δ</td><td>λω.(coh<sup>n,p</sup><sub>frame,ε,ω,q,p</sub>(d)(restr<sup>n-1,p</sup><sub>painting,ε,q</sub>(D.2)(l<sub>ω</sub>)))</td></tr><tr><td>restr<sup>n,p,p≤q≤n-1</sup><sub>painting,ε,q</sub></td><td>(D : νSet<sup>n</sup>)<br/>(E : νSet<sup>=n</sup>(D))<br/>(d : frame<sup>n,p</sup>(D))<br/>(c : painting<sup>n,p</sup>(E)(d))</td><td>:</td><td>painting<sup>n-1,p</sup>(D.2)(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>restr<sup>n,p,p=q</sup><sub>painting,ε,q</sub></td><td>D E d (l, __)</td><td>Δ</td><td>l<sub>ε</sub></td></tr><tr><td>restr<sup>n,p,p≤q</sup><sub>painting,ε,q</sub></td><td>D E d (l, c)</td><td>Δ</td><td>(restr<sup>n,p</sup><sub>layer,ε,q</sub>(l), restr<sup>n,p+1</sup><sub>painting,ε,q</sub>(E)(c))</td></tr></tbody></table>

<table><caption>Table 5': Commutation of q-th projection and r-th projection, or coherence conditions</caption><tbody><tr><td>coh<sup>n,p,p≤r≤q≤n-2</sup><sub>frame,ε,ω,q,r</sub></td><td>{D : νSet<sup>n</sup>}<br/>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>restr<sup>n-1,p</sup><sub>frame,ε,q</sub>(restr<sup>n,p</sup><sub>frame,ω,r</sub>(d))<br/>= restr<sup>n-1,p</sup><sub>frame,ω,r</sub>(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>coh<sup>n,0</sup><sub>frame,ε,ω,q,r</sub></td><td>D *</td><td>Δ</td><td>refl(*)</td></tr><tr><td>coh<sup>n,p'+1</sup><sub>frame,ε,ω,q,r</sub></td><td>D (d, l)</td><td>Δ</td><td>(coh<sup>n,p'</sup><sub>frame,ε,ω,q,r</sub>(d), coh<sup>n,p'</sup><sub>layer,ε,ω,q,r</sub>(l))</td></tr><tr><td>coh<sup>n,p,p<r≤q≤n-2</sup><sub>layer,ε,ω,q,r</sub></td><td>(D : νSet<sup>n</sup>)<br/>{d : frame<sup>n,p</sup>(D)}<br/>(l : layer<sup>n,p</sup>(d))</td><td>:</td><td>coh<sup>n,p</sup><sub>frame,ε,ω,q,r</sub>(d)(restr<sup>n-1,p</sup><sub>layer,ε,q</sub>(restr<sup>n,p</sup><sub>layer,ω,r</sub>(l)))<br/>= restr<sup>n-1,p</sup><sub>layer,ω,r</sub>(restr<sup>n,p</sup><sub>layer,ε,q+1</sub>(l))</td></tr><tr><td>coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub></td><td>D d l</td><td>Δ</td><td>λθ.(coh<sup>n,p</sup><sub>frame,ε,θ,q,r</sub>(d))(ap (coh<sup>n-1,p</sup><sub>frame,ω,θ,r,p</sub>(restr<sup>n,p</sup><sub>frame,ε,q+2</sub>(d))))<br/>(ap (restr<sup>n-1,p</sup><sub>frame,ω,r</sub>(coh<sup>n,p</sup><sub>frame,ε,θ,q+1,p</sub>))) coh<sup>n-1,p</sup><sub>painting,ε,ω,q-1,r-1</sub>(D.2)(l<sub>θ</sub>)</td></tr><tr><td>coh<sup>n,p,p≤r≤q≤n-2</sup><sub>painting,ε,ω,q,r</sub></td><td>(D : νSet<sup>n</sup>)<br/>(E : νSet<sup>=n</sup>(D))<br/>(d : frame<sup>n,p</sup>(D))<br/>(c : painting<sup>n,p</sup>(E)(d))</td><td>:</td><td>coh<sup>n,p</sup><sub>frame,ε,ω,q,r</sub>(d)(restr<sup>n-1,p</sup><sub>painting,ε,q</sub>(D.2)(restr<sup>n,p</sup><sub>painting,ω,r</sub>(E)(c)))<br/>= restr<sup>n-1,p</sup><sub>painting,ω,r</sub>(D.2)(restr<sup>n,p</sup><sub>painting,ε,q+1</sub>(E)(c))</td></tr><tr><td>coh<sup>n,p,p=r</sup><sub>painting,ε,ω,q,r</sub></td><td>D E d (l, __)</td><td>Δ</td><td>refl(restr<sup>n-1,p</sup><sub>painting,ε,q-1</sub>(D.2)(l<sub>ε</sub>))</td></tr><tr><td>coh<sup>n,p,p<r</sup><sub>painting,ε,ω,q,r</sub></td><td>D E d (l, c)</td><td>Δ</td><td>(coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub>(l), coh<sup>n,p+1</sup><sub>painting,ε,ω,q,r</sub>(E)(c))</td></tr></tbody></table>

The proof of $coh_{frame}$ itself requires making explicit several rewrites which were invisible in extensional type theory. The commutation of $restr_{layer}$ lives in a type referring to $coh_{frame}$, so we need a transport along the commutation of $restr_{frame}$ in the statement of $coh_{layer}$. The proof of $coh_{layer}$ is the most involved proof of the construction, as it requires a higher-dimensional coherence condition, $coh_2_{frame}$, whose exact formulation is as follows.

$$coh_{frame,ε,ω,q,r,p}^{n,p}(restr_{frame,ε,q+2}^{n,p}(d)) \bullet$$

$$ap restr_{frame,ω,r}^{n,p}(coh_{frame,ε,θ,q+1,p}^{n,p}(d)) \bullet$$

$$coh_{frame,ε,ω,q,r}^{n,p}(restr_{frame,θ,p}^{n,p}(d)) =$$

$$ap restr_{frame,θ,p}^{n,p}(coh_{frame,ε,ω,q+1,r+1}^{n,p}(d)) \bullet$$

$$coh_{frame,ε,θ,q,p}^{n,p}(restr_{frame,ω,r+1}^{n,p}(d)) \bullet$$

$$ap restr_{frame,ε,q}^{n,p}(coh_{frame,ω,θ,r,p}^{n,p}(d))$$

where ap applies a function on two sides of an equality, and $\bullet$ is transitivity of equality. This property of equality proofs holds in HSet, and since our construction is done in HSet, the term is trivially discharged.
So far, we have not paid attention to the fact that we have a dependent type, shown as $\Sigma$. To be more precise, note that $\text{fullframe}^n$ depends on all $X_i$ up to $n-1$. So, we need to package up $X_i$, for $i < n$, into a nesting of $\Sigma$-types, constituting the type of a $n$-truncated $\nu$-set, which we wrote $\nu\text{Set}^{<n}$. This allows us to give the type $\nu\text{Set}^{<n} \to \text{HSet}$ to $\text{fullframe}^n$. Then, for $D : \nu\text{Set}^{<n}$, representing an initial prefix of $X_0, X_1, \dots, X_{n-1}$, the indexed set $X_n$ has type $\text{fullframe}^n(D) \to \text{HSet}$. Thus, $\text{frame}^{n,p}$, $\text{layer}^{n,p}$ and $\text{painting}^{n,p}$ also depend on $D$. We can then reformulate the previous equation with its dependency on $D$. In particular, $X_n$ is just the last component of $D$, that is $D$.tl.

$$ 
\begin{align*}
\text{frame}^{n,p}(D) &\triangleq \Sigma a_n : (\dots (\Sigma^* : \text{unit. } \text{layer}^{n,0}(D)) \dots). \text{layer}^{n,p-1}(D) \\
\text{painting}^{n,p}(D) &\triangleq \Sigma l_p : \text{layer}^{n,p}(D). (\dots (\Sigma l_n : \text{layer}^{n,n-1}(D). D.\text{tl}) \dots)
\end{align*}
$$

An extra refinement arises from the fact that each new layer of a frame has to be glued onto the border of the partial frame built so far. So, each $\text{layer}^{n,p}$ has to depend on $\text{frame}^{n,p}$. We also need a way to characterize the $\nu$ borders of each $\text{painting}^{n-1,p}$ that composes a $\text{layer}^{n,p}$, and this is where the restriction $\text{restr}_{\text{frame},\epsilon,p}^{n,p}$ arrives, for each $\epsilon < \nu$. For instance, in the picture, the left and right faces (red), $\text{painting}^{2,1}$, are laid on respectively the left and right borders of the front and back faces (blue), and hence need to depend on $\text{frame}^{3,1}$. The left and right borders of the front and back faces are then extracted as $\text{restr}_{\text{frame},L}^{2,1}(D)(d)$ and $\text{restr}_{\text{frame},R}^{2,1}(D)(d)$. We can then refine again the previous equation by showing the dependencies on $d$, as shown below.

$$ 
\begin{align*}
\text{frame}^{n,p}(D) &\triangleq \Sigma d : (\dots (\Sigma^* : \text{unit. } \text{layer}^{n,0}(D)(\ast)) \dots). \text{layer}^{n,p}(D)(d) \\
\text{painting}^{n,p}(D)(d) &\triangleq \Sigma l_p : \text{layer}^{n,p}(D)(d). (\dots (\Sigma l_n : \text{layer}^{n,n-1}(D)(d, l_p, \dots, l_{n-1}). \\
&\qquad \qquad \qquad \qquad \qquad D.\text{tl}(d, l_p, \dots, l_n)) \dots) \\
&\qquad \text{where } (d, l_p, \dots, l_q) \text{ abbreviates } ((\dots (d, l_p), \dots), l_q)
\end{align*}
$$

When $\nu = 2$, using $L$ and $R$ to represent the sides, the formation of layers from paintings amounts to:

$$ \text{layer}^{n,p}(D)(d) \triangleq \text{painting}^{n-1,p}(D.hd)(\text{restr}_{\text{frame},L,p}^{n,p}(d)) \times \text{painting}^{n-1,p}(D.hd)(\text{restr}_{\text{frame},R,p}^{n,p}(d)) $$

The operation $\text{restr}_{\text{frame},\epsilon,q}^{n,p}$ restricts the $p$ first layers of a frame, and the construction is by recursion on the structure of a frame $d$. This necessitates the definitions $\text{restr}_{\text{layer},\epsilon,q}^{n,p}(d)(l)$ and $\text{restr}_{\text{painting},\epsilon,q}^{n,p}(d)(c)$, for $l$ a layer, and $c$ a painting. The key case is $\text{restr}_{\text{painting},\epsilon,p}^{n,p}(d)(c)$, where $c$, a $\text{painting}^{n,p}$, necessarily has the form of $((c_L, c_R), \_)$ . Here, $\text{restr}_{\text{painting},L,p}^{n,p}$ picks out $c_L$, a $\text{painting}^{n-1,p}$, $\text{restr}_{\text{painting},R,p}^{n,p}$ picks out the $c_R$, also a $\text{painting}^{n-1,p}$, and the last component, shown as $\_$, a $\text{painting}^{n,p+1}$, is discarded. There is one last difficulty, which we illustrate by writing down expected and actual types.

Given $c_\omega$ of type

$$ c_\omega : \text{painting}^{n-1,p}(D.hd)(\text{restr}_{\text{frame},\omega,p}^{n,p}(d)) $$

$\text{restr}_{\text{layer},\epsilon,q}^{n,p}(d)(c_L, c_R)$ produces a layer in which the $\omega$-component has the type

$$ \text{painting}^{n-2,p}(D.hd.hd)(\text{restr}_{\text{frame},\epsilon,q}^{n-1,p}(\text{restr}_{\text{frame},\omega,p}^{n,p}(d))) $$

while we expect a component of type

$$ \text{painting}^{n-2,p}(D.hd.hd)(\text{restr}_{\text{frame},\omega,p}^{n-1,p}(\text{restr}_{\text{frame},\epsilon,q+1}^{n,p}(d))) $$

Hence, we need a coherence condition to commute the restrictions. Coherence conditions similar to this necessitate what are shown as, $\text{coh}_{\text{frame}}$, $\text{coh}_{\text{layer}}$ and $\text{coh}_{\text{painting}}$ in table 5. These are by induction on the structure of frame, layer and painting. Note that, for the construction in intensional type theory, we further need a 2-dimensional coherence condition, $\text{coh}_2_{\text{frame}}$, for $\text{coh}_{\text{layer}}$, which is explained in the next section.

## V.3 From extensional to intensional type theory

In this section, we intend to get rid of the reflection rule and make explicit the equational reasoning step needed to rephrase the construction in intensional type theory. For readability purposes, we make only explicit in this section the key coherence conditions of the construction. Other cases of equality reasoning would have to be made explicit to fully obtain a construction in intensional type theory, but these steps are standard enough to be omitted at this stage. See section V.6 for the details.

The need for transport along a proof of commutation of $\text{restr}_{\text{frame}}$ in the definition of $\text{restr}_{\text{layer}}$ is made explicit in table 4', where the arrow over $\text{coh}_{\text{frame}}$ indicates the direction of rewrite.
Notice that each `restr` layer in the type of `coh` layer is hiding a `coh` frame rewrite: this makes a sum total of three `coh` frame rewrites on the left-hand side, and two `coh` frame rewrites on the right-hand side. In the proof term of `coh` layer, `coh` painting has one `coh` frame rewrite on its left-hand side. This, combined with the two terms of the form `ap coh` frame matches our expectation of three `coh` frame on the left-hand side, and two `coh` frame on the right-hand side. Then, `coh2` frame can be seen as expressing the commutation of these `coh` frame terms.

Finally, let us explain `coh` painting. The base case $p = r$ is the key case of the commutation of `restr` frame, when one of the `restr` painting collapses, and the remaining equation holds trivially. The case of $p < r$ follows the structure of `restr` painting by induction.

If we were not working in `HSet`, but in `HGpd` we would need to prove one more higher-dimensional coherence, and if we were working in `Type`, we would need to prove arbitrarily many higher-dimensional coherences. Here, `HGpd` is the subset of types `A` such that for all `x` and `y` in `A`, $x = y$ is in `HSet`. See [Her15, ACK16, Kra21] for a discussion on the need for recursive higher-dimensional coherence conditions in formulating higher-dimensional structures in type theory.

## V.4 Well-foundedness of the construction

Since the construction shown in the previous sections is by induction on `n`, and dependencies are on lower `n` and $p < n$, one would imagine formalizing this using well-founded induction in dependent type theory. We initially tried this approach, and had terms dependent on the proofs of the case distinction that $n' \le n$ implies $n' < n$ or $n' = n$, but these proofs did not come with enough definitional properties to be usable in practice. Hence, we chose a different route: in practice, since `restr` frame depends on `frame` `n` and `frame` $n-1$, while `coh` frame depends on `frame` $n$, `frame` $n-1$, and `frame` $n-2$, we only need to keep track of three consecutive dimensions. Hence, what we build by induction at level `n`, is a structure made not only of the definitions shown in the tables 3, 4', and 5', but also of `frame`, `layer`, `painting` at levels $n-1$ and $n-2$, as well as `restr` frame, `restr` layer, and `restr` painting at level $n-1$, together with helper equations.

## V.5 Dependencies in inequality proofs

The entire construction relies on inequalities over natural numbers, and we use two different definitions of $\le$ addressing different concerns in our formalization. In order to build our first variant, we use an intermediate “recursive definition” phrased as:

```
Fixpoint leR (n m : nat) : SProp :=
match n, m with
| O, _ => STrue
| S n, O => SFalse
| S n, S m => leR n m
end.
```

Here, `SProp` is a definitionally proof-irrelevant impredicative universe morally<sup>f</sup> living at the bottom of the universe hierarchy [GCST19]. By placing the definition in `SProp`, we have definitional equality of inequality proofs. However, for the purpose of unification, this definition does not go far enough. Consider the unification problems:

```
leR_trans ?p leR_refl = ?p
leR_trans leR_refl ?p = ?p
```

where `leR_trans` is transitivity, `leR_refl` is reflexivity, and ?p is an existential variable. These two problems definitionally hold in `SProp`, but equating them does not solve the existential variable. For unification to be useful in solving existential variables, we present our first variant of $\le$, which we dub as the “Yoneda variant”:

```
Definition leY n m :=
forall p, leR p n -> leR p m.
```

This definition is an improvement over `leR` since reflexivity is now definitionally the neutral element of transitivity, and associativity of transitivity also holds definitionally. Although it significantly eases our proof, there are some instances where unification is unable to solve the existential variables, and we have to provide them explicitly.

The second variant of $\le$, the “inductive variant”, is phrased as:

<footnote><sup>f</sup>In Coq ([The23b]), it is however a stand-alone universe unrelated to the universe hierarchy.</footnote>
<table><caption>**Table 4**: q-th projection of restr, or faces</caption><tbody><tr><td>restr<sup>n,p,p≤q≤n-1</sup><sub>frame,ε,q</sub></td><td>{D : vSet<sup>n</sup>}<br/>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>frame<sup>n-1,p</sup>(D.1)</td></tr><tr><td>restr<sup>n,0</sup><sub>frame,ε,q</sub></td><td>D*</td><td>Δ</td><td>*</td></tr><tr><td>restr<sup>n,p'+1</sup><sub>frame,ε,q</sub></td><td>D (d, l)</td><td>Δ</td><td>(restr<sup>n,p'</sup><sub>frame,ε,q</sub>(d), restr<sup>n,p'</sup><sub>layer,ε,q-1</sub>(l))</td></tr><tr><td>restr<sup>n,p,p≤q≤n-2</sup><sub>layer,ε,q</sub></td><td>{D : vSet<sup>n</sup>}<br/>{d : frame<sup>n,p</sup>(D)}<br/>(l : layer<sup>n,p</sup>(d))</td><td>:</td><td>layer<sup>n-1,p</sup>(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>restr<sup>n,p</sup><sub>layer,ε,q</sub></td><td>D dl</td><td>Δ</td><td>λω.(coh<sup>n,p</sup><sub>frame,ε,ω,q,p</sub>(d)(restr<sup>n-1,p</sup><sub>painting,ε,q</sub>(D.2)(l<sub>ω</sub>)))</td></tr><tr><td>restr<sup>n,p,p≤q≤n-1</sup><sub>painting,ε,q</sub></td><td>(D : vSet<sup>n</sup>)<br/>(E : vSet<sup>n</sup>(D))<br/>(d : frame<sup>n,p</sup>(D))<br/>(c : painting<sup>n,p</sup>(E)(d))</td><td>:</td><td>painting<sup>n-1,p</sup>(D.2)(restr<sup>n,p</sup><sub>frame,ε,q</sub>(d))</td></tr><tr><td>restr<sup>n,p,p=q</sup><sub>painting,ε,q</sub></td><td>D E d (l, _)</td><td>Δ</td><td>l<sub>ε</sub></td></tr><tr><td>restr<sup>n,p,p<q</sup><sub>painting,ε,q</sub></td><td>D E d (l, c)</td><td>Δ</td><td>(restr<sup>n,p</sup><sub>layer,ε,q-1</sub>(l), restr<sup>n,p+1</sup><sub>painting,ε,q</sub>(E)(c))</td></tr></tbody></table>

<table><caption>**Table 5**: Commutation of q-th projection and r-th projection, or coherence conditions</caption><tbody><tr><td>coh<sup>n,p,p≤r≤q≤n-2</sup><sub>frame,ε,ω,q,r</sub></td><td>{D : vSet<sup>n</sup>}<br/>(d : frame<sup>n,p</sup>(D))</td><td>:</td><td>restr<sup>n-1,p</sup><sub>frame,ε,q</sub>(restr<sup>n,p</sup><sub>frame,ω,r</sub>(d))<br/>= restr<sup>n-1,p</sup><sub>frame,ω,r</sub>(restr<sup>n,p</sup><sub>frame,ε,q+1</sub>(d))</td></tr><tr><td>coh<sup>n,0</sup><sub>frame,ε,ω,q,r</sub></td><td>D*</td><td>Δ</td><td>refl(*)</td></tr><tr><td>coh<sup>n,p'+1</sup><sub>frame,ε,ω,q,r</sub></td><td>D (d, l)</td><td>Δ</td><td>(coh<sup>n,p'</sup><sub>frame,ε,ω,q,r</sub>(d), coh<sup>n,p'</sup><sub>layer,ε,ω,q-1,r-1</sub>(l))</td></tr><tr><td>coh<sup>n,p,p≤r≤q≤n-3</sup><sub>layer,ε,ω,q,r</sub></td><td>{D : vSet<sup>n</sup>}<br/>{d : frame<sup>n,p</sup>(D)}<br/>(l : layer<sup>n,p</sup>(d))</td><td>:</td><td>coh<sup>n,p</sup><sub>frame,ε,ω,q+1,r+1</sub>(d)(restr<sup>n-1,p</sup><sub>layer,ε,q</sub>(restr<sup>n,p</sup><sub>layer,ω,r</sub>(l)))<br/>= restr<sup>n-1,p</sup><sub>layer,ω,r</sub>(restr<sup>n,p</sup><sub>layer,ε,q+1</sub>(l))</td></tr><tr><td>coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub></td><td>D dl</td><td>Δ</td><td>λθ.(coh<sup>n,p</sup><sub>frame,ε,ω,θ,q,r</sub>(d))(ap (coh<sup>n-1,p</sup><sub>frame,ω,θ,r,p</sub>(restr<sup>n,p</sup><sub>frame,ε,q+2</sub>(d))))<br/>(ap (restr<sup>n-2,p</sup><sub>frame,ω,r</sub>(coh<sup>n,p</sup><sub>frame,ε,θ,q+1,p</sub>))) coh<sup>n-1,p</sup><sub>painting,ε,ω,q,r</sub>(D.2)(l<sub>θ</sub>)</td></tr><tr><td>coh<sup>n,p,p≤r≤q≤n-2</sup><sub>painting,ε,ω,q,r</sub></td><td>{D : vSet<sup>n</sup>}<br/>(E : vSet<sup>n</sup>(D))<br/>{d : frame<sup>n,p</sup>(D)}<br/>(c : painting<sup>n,p</sup>(E)(d))</td><td>:</td><td>coh<sup>n,p</sup><sub>frame,ε,ω,q,r</sub>(d)(restr<sup>n-1,p</sup><sub>painting,ε,q</sub>(D.2)(restr<sup>n,p</sup><sub>painting,ω,r</sub>(E)(c)))<br/>= restr<sup>n-1,p</sup><sub>painting,ω,r</sub>(D.2)(restr<sup>n,p</sup><sub>painting,ε,q+1</sub>(E)(c))</td></tr><tr><td>coh<sup>n,p,p=r</sup><sub>painting,ε,ω,q,r</sub></td><td>D E d (l, _)</td><td>Δ</td><td>refl(restr<sup>n-1,p</sup><sub>painting,ε,q-1</sub>(D.2)(l<sub>ε</sub>))</td></tr><tr><td>coh<sup>n,p,p<r</sup><sub>painting,ε,ω,q,r</sub></td><td>D E d (l, c)</td><td>Δ</td><td>(coh<sup>n,p</sup><sub>layer,ε,ω,q,r</sub>(l), coh<sup>n,p+1</sup><sub>painting,ε,ω,q,r</sub>(E)(c))</td></tr></tbody></table>

The proof of $coh_{frame}$ itself requires making explicit several rewrites which were invisible in extensional type theory. The commutation of $restr_{layer}$ lives in a type referring to $coh_{frame}$, so we need a transport along the commutation of $restr_{frame}$ in the statement of $coh_{layer}$. The proof of $coh_{layer}$ is the most involved proof of the construction, as it requires a higher-dimensional coherence condition, $coh_{2frame}$, whose exact formulation is as follows.

$$ \begin{align*} & \mathrm{coh}_{\mathrm{frame},\omega,\theta,r,p}^{n-1,p}(\mathrm{restr}_{\mathrm{frame},\epsilon,q+2}^{n,p}(d)) \bullet \\ & \mathrm{ap} \ \mathrm{restr}_{\mathrm{frame},\omega,r}^{n-2,p}(\mathrm{coh}_{\mathrm{frame},\epsilon,\theta,q+1,p}^{n,p}(d)) \bullet \\ & \mathrm{coh}_{\mathrm{frame},\epsilon,\omega,q,r}^{n-1,p}(\mathrm{restr}_{\mathrm{frame},\theta,p}^{n,p}(d)) = \\ & \mathrm{ap} \ \mathrm{restr}_{\mathrm{frame},\theta,p}^{n-2,p}(\mathrm{coh}_{\mathrm{frame},\epsilon,\omega,q+1,r+1}^{n,p}(d)) \bullet \\ & \mathrm{coh}_{\mathrm{frame},\epsilon,\theta,q,p}^{n-1,p}(\mathrm{restr}_{\mathrm{frame},\omega,r+1}^{n,p}(d)) \bullet \\ & \mathrm{ap} \ \mathrm{restr}_{\mathrm{frame},\epsilon,q}^{n-2,p}(\mathrm{coh}_{\mathrm{frame},\omega,\theta,r,p}^{n,p}(d)) \end{align*} $$

where ap applies a function on two sides of an equality, and $\bullet$ is transitivity of equality. This property of equality proofs holds in HSet, and since our construction is done in HSet, the term is trivially discharged.

Notice that each $restr_{layer}$ in the type of $coh_{layer}$ is hiding a $coh_{frame}$ rewrite: this makes a sum total of three $coh_{frame}$ rewrites on the left-hand side, and two $coh_{frame}$ rewrites on the right-hand side. In the proof term
Inductive $leI : nat \to nat \to Type :=$
| $leI\_refl n : n < \sim n$
| $leI\_down \{n p\} : p.+1 < \sim n \to p < \sim n$
where "$n < \sim m$" := ($leI n m$) : nat\_scope.

Compared to $leY$, $leI$ has no proof-irrelevance properties. This definition is specially crafted for *painting*, where we have to reason inductively from $p \le n$ to $n$. In our usage, we have lemmas $leY\_of\_leI$ and $leI\_of\_leY$ in order to equip $leY$ with the induction scheme of $leI$. The resulting induction scheme has computational rules holding propositionally.

## V.6 Groupoid properties of equality and basic type isomorphisms

The construction relies on groupoid properties of equality which are left implicit in table 5'. The use of the equivalence between $u = v$ and $\Sigma(p : u.hd = v.hd)$.($u.tl = v.tl$) for $u$ and $v$ in a $\Sigma$-type is left implicit in the same table. Also implicit is the use of the equivalence between $f = g$ and $\Pi a : A. f(a) = g(a)$ for $f$ and $g$ in $\Pi a : A. B$, where it should be recalled that the right-to-left map, or functional extensionality, holds by default in extensional type theory. These have to be made explicit in the formalization.

As a final remark, note that as a consequence of $\eta$-conversion for finite enumerated types, the requirement of functional extensionality disappears when $\nu$ is finite. However, this is a conversion which Coq does not implement, and the alternative would be to replace $\Pi a : \nu. B$ by a “flat” iterated product $B(1) \times B(2) \times \dots \times B(\nu)$.

# VI FUTURE WORK

The construction could be extended with degeneracies as well as with permutations [GM03]. Dependent $\nu$-sets could also be defined, opening the way to construct $\Pi$-types and $\Sigma$-types of $\nu$-sets. A $\nu$-set of $\nu$-sets representing a universe could also be defined as sketched in a talk at the HoTT-UF workshop for the bridge case ([Her20]). More generally, we believe these lines of work would eventually provide alternative models to parametric type theories [NVD17, CH20] where equality of types, now a family rather than the total space of a fibration, is not only definitionally isomorphic to bridges [BCM15], but definitionally the same as bridges.

By equipping the universe construction with a structure of equivalences, as suggested along the lines of [AK15], we also suspect the construction to be able to serve as a basis for syntactic models of various versions of cubical type theory [BCH13, CCHM18, ABC$^+$$21$], saving the detour via the fibered approach inherent to usual presheaf models. In particular, we conjecture being able to justify univalence holding definitionally. Our approach would also firmly ground cubical type theory in iterated parametricity.

Another direction for future work is to give a general definition of presheaf in indexed form over a direct category, and to show the equivalence with the standard definition of presheaf.

## REFERENCES

[ABC$^+$$21$] Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of cartesian cubical type theory. *Math. Struct. Comput. Sci.*, 31(4):424–468, 2021.

[ACK16] 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.

[ACK17] Danil Annenkov, Paolo Capriotti, and Nicolai Kraus. Two-level type theory and applications. *CoRR*, abs/1705.03307, 2017.

[AGJ14] Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In *The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014.*, 2014.

[AK15] Thorsten Altenkirch and Ambrus Kaposi. Towards a cubical type theory without an interval. In Tarmo Uustalu, editor, *21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia*, volume 69 of LIPIcs, pages 3:1–3:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.

[BCH13] Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In Ralph Matthes and Aleksy Schubert, editors, *19th International Conference on Types for Proofs and Types 2013*, 2013.
of $\operatorname{coh}_{\text{layer}}$, $\operatorname{coh}_{\text{painting}}$ has one $\operatorname{coh}_{\text{frame}}$ rewrite on its left-hand side. This, combined with the two terms of the form $\operatorname{coh}_{\text{frame}}$, matches our expectation of three $\operatorname{coh}_{\text{frame}}$ on the left-hand side, and two $\operatorname{coh}_{\text{frame}}$ on the right-hand side. Then, $\operatorname{coh}_{2\text{frame}}$ can be seen as expressing the commutation of these $\operatorname{coh}_{\text{frame}}$ terms.

Finally, let us explain $\operatorname{coh}_{\text{painting}}$. The base case $p = r$ is the key case of the commutation of $\operatorname{restr}_{\text{frame}}$, when one of the $\operatorname{restr}_{\text{painting}}$ collapses, and the remaining equation holds trivially. The case of $p < r$ follows the structure of $\operatorname{restr}_{\text{painting}}$ by induction.

If we were not working in $\mathcal{HSet}$, but in $\mathcal{HGpd}$ we would need to prove one more higher-dimensional coherence, and if we were working in Type, we would need to prove arbitrarily many higher-dimensional coherencees. Here, $\mathcal{HGpd}$ is the subset of types $A$ such that for all $x$ and $y$ in $A$, $x = y$ is in $\mathcal{HSet}$. See [Her15, ACK16, Kra21] for a discussion on the need for recursive higher-dimensional coherence conditions in formulating higher-dimensional structures in type theory.

## V.4 Well-foundedness of the construction

Since the construction shown in the previous sections is by induction on $n$, and dependencies are on lower $n$ and $p < n$, one would imagine formalizing this using well-founded induction in dependent type theory. We initially tried this approach, and had terms dependent on the proofs of the case distinction that $n' \le n$ implies $n' < n$ or $n' = n$, but these proofs did not come with enough definitional properties to be usable in practice. Hence, we chose a different route: in practice, since $\operatorname{restr}_{\text{frame}}^n$ depends on $\text{frame}^n$ and $\text{frame}^{n-1}$, while $\operatorname{coh}_{\text{frame}}^n$ depends on $\text{frame}^n$, $\text{frame}^{n-1}$, and $\text{frame}^{n-2}$, we only need to keep track of three consecutive dimensions. Hence, what we build by induction at level $n$, is a structure made not only of the definitions shown in the tables 3, 4', and 5', but also of frame, layer, painting at levels $n-1$ and $n-2$, as well as $\operatorname{restr}_{\text{frame}}$, $\operatorname{restr}_{\text{layer}}$, and $\operatorname{restr}_{\text{painting}}$ at level $n-1$, together with helper equations.

## V.5 Dependencies in inequality proofs

The entire construction relies on inequalities over natural numbers, and we use two different definitions of $\le$ addressing different concerns in our formalization. In order to build our first variant, we use an intermediate "recursive definition" phrased as:

```hottag
Fixpoint leR (n m : nat) : SProp :=
match n, m with
| O, _ => STrue
| S n, O => SFalse
| S n, S m => leR n m
end.
```

Here, $SProp$ is a definitionally proof-irrelevant impredicative universe morally$^f$ living at the bottom of the universe hierarchy [GCST19]. By placing the definition in $SProp$, we have definitional equality of inequality proofs. However, for the purpose of unification, this definition does not go far enough. Consider the unification problems:

```
leR_trans ?p leR_refl = ?p
leR_trans leR_refl ?p = ?p
```

where $leR_trans$ is transitivity, $leR_refl$ is reflexivity, and $?p$ is an existential variable. These two problems definitionally hold in $SProp$, but equating them does not solve the existential variable. For unification to be useful in solving existential variables, we present our first variant of $\le$, which we dub as the "Yoneda variant":

```hottag
Definition leY n m :=
forall p, leR p n -> leR p m.
```

This definition is an improvement over $leR$ since reflexivity is now definitionally the neutral element of transitivity, and associativity of transitivity also holds definitionally. Although it significantly eases our proof, there are some instances where unification is unable to solve the existential variables, and we have to provide them explicitly.

The second variant of $\le$, the "inductive variant", is phrased as:

```hottag
Inductive leI : nat -> nat -> Type :=
| leI_refl n : n <~ n
| leI_down {n p} : p.+1 <~ n -> p <~ n
where "n <~ m" := (leI n m) : nat_scope.
```

<footnote>$^f$In Coq, it is however a stand-alone universe unrelated to the universe hierarchy.</footnote>
and *Programs, TYPES 2013, April 22-26, 2013, Toulouse, France*, volume 26 of LIPIcs, pages 107–128. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.

[BCM15] Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. A presheaf model of parametric type theory. *Electr. Notes Theor. Comput. Sci.*, 319:67–82, 2015.

[BJP10] Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Parametricity and dependent types. In Paul Hudak and Stephanie Weirich, editors, *Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010*, pages 345–356. ACM, 2010.

[BL11] Jean-Philippe Bernardy and Marc Lasson. Realizability and parametricity in pure type systems. In *Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings*, volume 6604 of Lecture Notes in Computer Science, pages 108–122. Springer, 2011.

[BM12] Jean-Philippe Bernardy and Guilhem Moulin. A computational interpretation of parametricity. In *2012 27th Annual IEEE Symposium on Logic in Computer Science*, pages 135–144. IEEE, 2012.

[BM17] Ulrik Buchholtz and Edward Morehouse. Varieties of cubical sets. In *International Conference on Relational and Algebraic Methods in Computer Science*, pages 77–92. Springer, 2017.

[CCHM18] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtsberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, *TYPES 2015*, volume 69 of LIPIcs, pages 5:1–5:34. Schloss Dagstuhl, 2018.

[CGH14] Pierre-Louis Curien, Richard Garner, and Martin Hofmann. Revisiting the categorical interpretation of dependent type theory. *Theoretical Computer Science*, 546:99–119, 2014. Models of Interaction: Essays in Honour of Glynn Winskel.

[CH20] Evan Cavallo and Robert Harper. Internal Parametricity for Cubical Type Theory. In Maribel Fernández and Anca Muscholl, editors, *28th EACSL Annual Conference on Computer Science Logic (CSL 2020)*, volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1–13:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[dMKA<sup>+</sup>15] Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, *Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings*, volume 9195 of Lecture Notes in Computer Science, pages 378–388. Springer, 2015.

[GCST19] Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. *Proc. ACM Program. Lang.*, 3(POPL):3:1–3:28, 2019.

[GM03] Marco Grandis and Luca Mauri. Cubical sets and their site. *Theory and Applications of Categories*, 11:185–211, 2003.

[Her15] Hugo Herbelin. A dependently-typed construction of semi-simplicial types. *Mathematical Structures in Computer Science*, 25(5):1116–1131, 2015.

[Her20] Hugo Herbelin. Investigations into syntactic iterated parametricity and cubical type theory, 2020.

[Hof95] Martin Hofmann. *Extensional concepts in intensional type theory*. Phd, University of Edinburgh, 1995.

[JS17] Patricia Johann and Kristina Sojakova. Cubical categories for higher-dimensional parametricity. *CoRR*, abs/1701.06244, 2017.

[KL21] Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after voevodsky). *Journal of the European Mathematical Society*, 23(6):2071–2126, 2021.

[Kra21] 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.

[Las14] Marc Lasson. *Réalisabilité et Paramétricité dans les Systèmes de Types Purs*. Ph.D. thesis, Université de Lyon, November 2014.

[LR20] Fosco Loregian and Emily Riehl. Categorical notions of fibration. *Expositiones Mathematicae*, 38(4):496–514, 2020.

[Mar84] Per Martin-Löf. *Intuitionistic type theory*, volume 1 of *Studies in proof theory*. Bibliopolis, 1984.

[ML75] Per Martin-Löf. An intuitionistic theory of types, predicative part. In *Logic Colloquium*, pages 73–118. North Holland, 1975.
Compared to leY, leI has no proof-irrelevance properties. This definition is specially crafted for *painting*, where we have to reason inductively from $p \le n$ to $n$. In our usage, we have lemmas `leY_of_leI` and `leI_of_leY` in order to equip leY with the induction scheme of leI. The resulting induction scheme has computational rules holding propositionally.

## V.6 Groupoid properties of equality and basic type isomorphisms

The construction relies on groupoid properties of equality which are left implicit in table 5'. The use of the equivalence between $u = v$ and $\Sigma(p : u.hd = v.hd)$.($u.tl = v.tl$) for $u$ and $v$ in a $\Sigma$-type is left implicit in the same table. Also implicit is the use of the equivalence between $f = g$ and $\Pi a : A. f(a) = g(a)$ for $f$ and $g$ in $\Pi a : A. B$, where it should be recalled that the right-to-left map, or functional extensionality, holds by default in extensional type theory. These have to be made explicit in the formalization.

As a final remark, note that as a consequence of $\eta$-conversion for finite enumerated types, the requirement of functional extensionality disappears when $v$ is finite. However, this is a conversion which Coq does not implement, and the alternative would be to replace $\Pi a : v.B$ by a "flat" iterated product $B(1) \times B(2) \times \dots \times B(v)$.

# VI FUTURE WORK

The construction could be extended with degeneracies as well as with permutations [GM03]. Dependent $v$-sets could also be defined, opening the way to construct $\Pi$-types and $\Sigma$-types of $v$-sets. A $v$-set of $v$-sets representing a universe could also be defined as sketched in a talk at the HoTT-UF workshop for the bridge case ([Her20]). More generally, we believe these lines of work would eventually provide alternative models to parametric type theories [NVD17, CH20] where equality of types, now a family rather than the total space of a fibration, is not only definitionally isomorphic to bridges [BCM15], but definitionally the same as bridges.

By equipping the universe construction with a structure of equivalences, as suggested along the lines of [AK15], we also suspect the construction to be able to serve as a basis for syntactic models of various versions of cubical type theory [BCH13a, CCHM18, ABC$^+21$], saving the detour via the fibred approach inherent to usual presheaf models. In particular, we conjecture being able to justify univalence holding definitionally. Our approach would also firmly ground cubical type theory in iterated parametricity.

Although prior approaches to constructing the indexed presentation of a presheaf over a direct category rely on it being evident by inspection that the fibred and indexed presentations are equivalent, no formal proof has been given, and this is a direction for future work. In our construction, we can check by computation of the first levels that it indeed computes the expected sets.

## REFERENCES

[ABC$^+21$] Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of cartesian cubical type theory. *Math. Struct. Comput. Sci.*, 31(4):424–468, 2021.

[ACK16] 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.

[ACK17] Danil Annenkov, Paolo Capriotti, and Nicolai Kraus. Two-level type theory and applications. *CoRR*, abs/1705.03307, 2017.

[ACKS23] Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. *Mathematical Structures in Computer Science*, 33(8):688–743, 2023.

[AGJ14] Robert Atkey, Neil Ghani, and Patricia Johann. A relationally parametric model of dependent type theory. In *The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014.*, 2014.

[AK15] Thorsten Altenkirch and Ambrus Kaposi. Towards a cubical type theory without an interval. In Tarmo Uustalu, editor, *21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia*, volume 69 of *LIPIcs*, pages 3:1–3:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.

[BCH13a] Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In Ralph Matthes and Aleksy Schubert, editors, *19th International Conference on Types for Proofs and Types 2013*, 2013.
[Moe21] Hugo Moeneclaey. Parametricity and semi-cubical types. In *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021*, pages 1-11. IEEE, 2021.

[Moe22] Hugo Moeneclaey. Cubical models are cofreely parametric. PhD thesis, Université Paris Cité, 2022.

[Mou16] Guilhem Moulin. *Internalizing parametricity*. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, 2016.

[NVD17] Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. Parametric quantifiers for dependent type theory. *Proc. ACM Program. Lang.*, 1(ICFP), aug 2017.

[PL15] Fedor Part and Zhaohui Luo. Semi-simplicial types in logic-enriched homotopy type theory. *CoRR*, abs/1506.04998, 2015.

[Rey83] John C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, *Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983*, pages 513-523. North-Holland/IFIP, 1983.

[The13] The Univalent Foundations Program. *Homotopy Type Theory: Univalent Foundations of Mathematics*. Institute for Advanced Study, 2013.

[The23a] The Agda Team. *Agda User Manual, Release 2.6.4*, Jan 2023.

[The23b] The Coq Development Team. *The Coq Reference Manual, version 8.18.0*, Jul 2023.

[Voe12] Vladimir Voevodsky. Semi-simplicial types, Nov 2012. Briefly described in Section 8 of [Her15].
and *Programs, TYPES 2013, April 22-26, 2013, Toulouse, France*, volume 26 of LIPIcs, pages 107–128. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.

[BCH13b] Marc Bezem, Thierry Coquand, and Simon Huber. A model of type theory in cubical sets. In Ralph Matthes and Aleksy Schubert, editors, *19th International Conference on Types for Proofs and Programs, TYPES 2013, April 22-26, 2013, Toulouse, France*, volume 26 of LIPIcs, pages 107–128. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.

[BCM15] Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. A presheaf model of parametric type theory. *Electr. Notes Theor. Comput. Sci.*, 319:67–82, 2015.

[BJP10] Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. Parametricity and dependent types. In Paul Hudak and Stephanie Weirich, editors, *Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010*, pages 345–356. ACM, 2010.

[BL11] Jean-Philippe Bernardy and Marc Lasson. Realizability and parametricity in pure type systems. In *Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings*, volume 6604 of Lecture Notes in Computer Science, pages 108–122. Springer, 2011.

[BM12] Jean-Philippe Bernardy and Guilhem Moulin. A computational interpretation of parametricity. In *2012 27th Annual IEEE Symposium on Logic in Computer Science*, pages 135–144. IEEE, 2012.

[BM17] Ulrik Buchholtz and Edward Morehouse. Varieties of cubical sets. In *International Conference on Relational and Algebraic Methods in Computer Science*, pages 77–92. Springer, 2017.

[CCHM15] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: A constructive interpretation of the univalence axiom. In Tarmo Uustalu, editor, *21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia*, volume 69 of LIPIcs, pages 5:1–5:34. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.

[CCHM18] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, *TYPES 2015*, volume 69 of LIPIcs, pages 5:1–5:34. Schloss Dagstuhl, 2018.

[CGH14] Pierre-Louis Curien, Richard Garner, and Martin Hofmann. Revisiting the categorical interpretation of dependent type theory. *Theoretical Computer Science*, 546:99–119, 2014. Models of Interaction: Essays in Honour of Glynn Winskel.

[CH20] Evan Cavallo and Robert Harper. Internal Parametricity for Cubical Type Theory. In Maribel Fernández and Anca Muscholl, editors, *28th EACSL Annual Conference on Computer Science Logic (CSL 2020)*, volume 152 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 13:1–13:17, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[GCST19] Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. *Proc. ACM Program. Lang.*, 3(POPL):3:1–3:28, 2019.

[GM03] Marco Grandis and Luca Mauri. Cubical sets and their site. *Theory and Applications of Categories*, 11:185–211, 2003.

[Her15] Hugo Herbelin. A dependently-typed construction of semi-simplicial types. *Mathematical Structures in Computer Science*, 25(5):1116–1131, 2015.

[Her20] Hugo Herbelin. Investigations into syntactic iterated parametricity and cubical type theory, 2020. Available at https://hott-uf.github.io/2020/HoTTUF_2020_paper_22.pdf.

[Hof95] Martin Hofmann. *Extensional concepts in intensional type theory*. PhD thesis, University of Edinburgh, 1995.

[HS94] Martin Hofmann and Thomas Streicher. The groupoid model refutes uniqueness of identity proofs. In *Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94)*, *Paris, France, July 4-7, 1994*, pages 208–212. IEEE Computer Society, 1994.

[JS17] Patricia Johann and Kristina Sojakova. Cubical categories for higher-dimensional parametricity. *CoRR*, abs/1701.06244, 2017.

[KL21] Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of Univalent Foundations (after Voevodsky). *Journal of the European Mathematical Society*, 23(6):2071–2126, 2021.

[Kra21] 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.

[KS17] Nicolai Kraus and Christian Sattler. Space-valued diagrams, type-theoretically. *arXiv preprint arXiv:1704.04543*, 2017.
[Las14] Marc Lasson. *Réalisabilité et Paramétricité dans les Systèmes de Types Purs*. PhD thesis, Université de Lyon, Nov 2014.

[LR20] Fosco Loregian and Emily Riehl. Categorical notions of fibration. *Expositiones Mathematicae*, 38(4):496-514, 2020.

[Mar84] Per Martin-Löf. *Intuitionistic type theory*, volume 1 of *Studies in proof theory*. Bibliopolis, 1984.

[ML75] Per Martin-Löf. An intuitionistic theory of types, predicative part. In *Logic Colloquium*, pages 73-118. North Holland, 1975.

[Moe21] Hugo Moeneclaey. Parametricity and semi-cubical types. In *36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021*, pages 1-11. IEEE, 2021.

[Moe22] Hugo Moeneclaey. *Cubical models are cofreely parametric*. PhD thesis, Université Paris Cité, 2022.

[Mou16] Guilhem Moulin. *Internalizing parametricity*. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, 2016.

[ND24] Andreas Nuyts and Dominique Devriese. Transpension: The Right Adjoint to the Pi-type. *Logical Methods in Computer Science*, Volume 20, Issue 2, June 2024.

[NVD17] Andreas Nuyts, Andrea Vezzosi, and Dominique Devriese. Parametric quantifiers for dependent type theory. *Proc. ACM Program. Lang.*, 1(ICFP), aug 2017.

[PL15] Fedor Part and Zhaohui Luo. Semi-simplicial types in logic-enriched homotopy type theory. *CoRR*, abs/1506.04998, 2015.

[Rey83] John C. Reynolds. Types, abstraction and parametric polymorphism. In R. E. A. Mason, editor, *Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983*, pages 513-523. North-Holland/IFIP, 1983.

[Shu15] Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. *Mathematical Structures in Computer Science*, 25(5):1203-1277, 2015.

[The13] The Univalent Foundations Program. *Homotopy Type Theory: Univalent Foundations of Mathematics*. Institute for Advanced Study, 2013.

[Voe12] Vladimir Voevodsky. Semi-simplicial types, Nov 2012. Briefly described in Section 8 of [Her15].
# APPENDIX: DEFINITION OF DEPENDENT STREAM

type formation

$\Gamma \vdash A : \mathbf{Type}_m$

$\Gamma, a : A \vdash B(a) : \mathbf{Type}_m$

$\Gamma, a : A, b : B(a) \vdash f(a, b) : A$

$\Gamma \vdash u : A$

$\Gamma \vdash \mathit{Stream}_{A,B,f} u : \mathbf{Type}_m$

introduction and eliminations

$\Gamma \vdash A : \mathbf{Type}_m$

$\Gamma, a : A \vdash B(a) : \mathbf{Type}_m$

$\Gamma, a : A, b : B(a) \vdash f(a, b) : A$

$\Gamma \vdash u : A$

$\Gamma, a : A \vdash D(a) : \mathbf{Type}_m$

$\Gamma \vdash w : D(u)$

$\Gamma, a : A, d : D(a) \vdash v(a, d) : B(a)$

$\Gamma, a : A, d : D(a) \vdash s(a, d) : D(f(a, v(a, d)))$

$\Gamma \vdash \mathit{cofix}_{a,d,g}^{u,w} \{ \mathit{this} := v(a,d); \mathit{next} := g(f(a,v(a,d)), s(a,d)) \} : \mathit{Stream}_{A,B,f} u$

$\Gamma \vdash t : \mathit{Stream}_{A,B,f} u$

$\Gamma \vdash t.\mathit{this} : B(u)$

$\Gamma \vdash t : \mathit{Stream}_{A,B,f} u$

$\Gamma \vdash t.\mathit{next} : \mathit{Stream}_{A,B,f} f(u, t.\mathit{this})$

computation

$\Gamma \vdash A : \mathbf{Type}_m$

$\Gamma, a : A \vdash B(a) : \mathbf{Type}_m$

$\Gamma, a : A, b : B(a) \vdash f(a, b) : A$

$\Gamma \vdash u : A$

$\Gamma, a : A \vdash D(a) : \mathbf{Type}_m$

$\Gamma \vdash w : D(u)$

$\Gamma, a : A, d : D(a) \vdash v(a, d) : B(a)$

$\Gamma, a : A, d : D(a) \vdash s(a, d) : D(f(a, v(a, d)))$

$\Gamma \vdash \mathit{cofix}_{a,d,g}^{u,w} \{ \mathit{this} := v(a,d); \mathit{next} := g(f(a,v(a,d)), s(a,d)) \}. \mathit{this} \equiv v(u,w) : B(u)$

$\Gamma \vdash A : \mathbf{Type}_m$

$\Gamma, a : A \vdash B(a) : \mathbf{Type}_m$

$\Gamma, a : A, b : B(a) \vdash f(a, b) : A$

$\Gamma \vdash u : A$

$\Gamma, a : A \vdash D(a) : \mathbf{Type}_m$

$\Gamma \vdash w : D(u)$

$\Gamma, a : A, d : D(a) \vdash v(a, d) : B(a)$

$\Gamma, a : A, d : D(a) \vdash s(a, d) : D(f(a, v(a, d)))$

$\Gamma \vdash \mathit{cofix}_{a,d,g}^{u,w} \{ \mathit{this} := v(a,d); \mathit{next} := g(f(a,v(a,d)), s(a,d)) \}. \mathit{next} \equiv \mathit{cofix}_{a,d,g}^{f(u,v(u,w)), s(u,w)} \{ \mathit{this} := v(a,d); \mathit{next} := g(f(a,v(a,d)), s(a,d)) \}$

$: \mathit{Stream}_{A,B,f} f(u, v(u, w))$

where $\mathit{cofix}_{a,d,g}^{u,w} \{ \mathit{this} := v(a,d); \mathit{next} := g(f(a,v(a,d)), s(a,d)) \}$ is a notation for the instantiation on parameter $u$ and internal value $w$ of the corecursive definition of a stream over an arbitrary $a$ generated by a recipe dependent on an arbitrary internal value $d : D(a)$ with first component given by $v(a,d)$ and second component given by $g(f(a,v(a,d)), s(a,d))$ where $g$, typed as $\Gamma, a : A, d : D(a) \vdash g(a,d) : \mathit{Stream}_{A,B,f} (f(a,d))$, formally represents the recursive call, and where $s(a,d)$ tells how the internal value evolves.