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

HAL
open science

# A dependently-typed construction of semi-simplicial types

Hugo Herbelin

► To cite this version:

Hugo Herbelin. A dependently-typed construction of semi-simplicial types. Mathematical Structures in Computer Science, 2015, From type theory and homotopy theory to Univalent Foundations of Mathematics, 25 (Special issue 05), pp.16. 10.1017/S0960129514000528. hal-00935446

HAL Id: hal-00935446

https://inria.hal.science/hal-00935446

Submitted on 23 Jan 2014

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 4.0 International License
# A dependently-typed construction of semi-simplicial types

Hugo Herbelin†

INRIA, PPS, Université Paris-Diderot

Received 20 January 2014

This paper presents a dependently-typed construction of semi-simplicial sets in type
theory where sets are taken to be types. This addresses an open question raised on the
wiki of the special year on Univalent Foundations at the Institute of Advanced Study
(2012-2013).

## 1. Introduction

A semi-simplicial set (or Delta-set) is a family of sets

$X_0$ (points)

$X_1$ (line segments)

$X_2$ (triangles)

$X_3$ (tetrahedra)

$\vdots$

$X_n$ (n-simplices)

$\vdots$

equipped with face operators $d_i^n : X_n \to X_{n-1}$ for $n \ge 1$ and $0 \le i \le n$ satisfying
$d_i^n \circ d_j^{n+1} = d_j^n \circ d_{i+1}^{n+1}$ for $n \ge i \ge j \ge 0$. See e.g. (Friedman, 2012) for more on the ideas
underlying semi-simplicial and simplicial sets.

Each element $x \in X_{n+1}$ can be canonically associated to the set of its faces $\{d_i^n(x) | 0 \le i \le n\}$, the set of the faces of its faces $\{d_i^{n-1}(d_j^n(x)) | 0 \le j \le i \le n-1\}$, etc. Hence, a

<footnote>† This research has been supported by a grant from the Fund for Math while staying at the Institute of Advanced Study in Fall 2012.</footnote>
semi-simplicial set can equivalently be represented as the following family of sets:

$$X_0$$
$$\Sigma a, b : X_0. \{x : X_1 | d_1^1(x) = a, d_0^1(x) = b\}$$
$$\Sigma a, b, c : X_0. \left\{ \begin{array}{l} \Sigma x : \{x : X_1 | d_1^1(x) = a, d_0^1(x) = b\} \\ \Sigma y : \{x : X_1 | d_1^1(x) = a, d_0^1(x) = c\} \\ \Sigma z : \{x : X_1 | d_1^1(x) = b, d_0^1(x) = c\} \end{array} \right\} . \{t : X_2\} \left\{ \begin{array}{l} d_2^2(t) = x \\ d_1^2(t) = y \\ d_0^2(t) = z \end{array} \right\}$$
$$\vdots$$

i.e. as:

$$Y_0$$
$$\Sigma a, b : Y_0. Y_1(a, b)$$
$$\Sigma a, b, c : Y_0. \left\{ \begin{array}{l} \Sigma x : Y_1(a, b) \\ \Sigma y : Y_1(a, c) \\ \Sigma z : Y_1(b, c) \end{array} \right\} . Y_2(a, b, c, x, y, z)$$
$$\vdots$$

where we have set:

$$Y_0 \triangleq X_0$$
$$Y_1(a, b) \triangleq \{x : X_1 | d_1^1(x) = a, d_0^1(x) = b\} \quad \text{for } a, b : Y_0$$
$$Y_2(a, b, c, x, y, z) \triangleq \left\{ \begin{array}{l} t : X_2 | d_2^2(t) = x, d_1^2(t) = y, d_0^2(t) = z \\ \text{for } a, b, c : Y_0, x : Y_1(a, b) \\ y : Y_1(a, c), z : Y_1(b, c) \end{array} \right.$$

Under this representation, each $X_n$ is tupled with its “skeleton” of faces at all levels $p < n$. Faces are now part of the structure of the sets of simplices and they can be retrieved by mere projection. In particular, for fixed $n$, $i$ and $j$, the equation $d_i^n \circ d_j^{n+1} = d_j^n \circ d_{i+1}^{n+1}$ for $n \ge i \ge j$ holds by construction.

Obviously, knowing the $Y_n$'s allows to reconstruct the $X_n$'s. Now, by taking the $Y_n$'s as the primitive objects, it becomes possible to define semi-simplicial sets without having to axiomatize the equational properties of faces, what is interesting in the context of homotopy type theory. Indeed, homotopy type theory is able to talk about types whose homotopic structure, in contrast to the homotopic structure of sets, is non degenerated and it is then natural to expect in this context a notion of “semi-simplicial types”. Additionally, the default equality of homotopy type theory is not strict, so that axiomatizing the equational properties of faces would automatically imply having to axiomatize also coherence diagrams (e.g. one has to assert that the two ways to prove $d_k^n \circ d_j^{n+1} \circ d_i^{n+2} = d_i^n \circ d_{j+1}^{n+1} \circ d_{k+2}^{n+2}$ for $0 \le i \le j \le k \le n$ are themselves equal, and, further, the same for arbitrary larger new such diagrams).

The idea to construct semi-simplicial types as dependently-typed families of sets of the form of the $Y_n$'s above started to circulate in between Carnegie-Mellon University and the Institute of Advanced Study (IAS), with Steve Awodey, Peter LeFanu Lumsdaine and others. Then, at the time the special year on Univalent Foundations started at the IAS, this was raised as an open problem by Peter LeFanu Lumsdaine on the wiki of the program (LeFanu Lumsdaine, 2012): How to define $Y_n$ as a formula of $n$? Can we define
a type of semi-simplicial types with $n$ semi-simplices for all $n$? Would this solve the need for arbitrary large coherence problems? Would it scale to simplicial types?

The current paper provides the following contributions to these questions:

- We propose a generic definition of the $Y_n$'s (Sections 2 to 5) which provides with a precise coinductive definition of a dependently-typed presentation of semi-simplicial types (Section 7). Actually, so as to have a slightly smoother definition, what we define in practice are semi-simplicial types augmented with a type $Y_{-1}$ of $(-1)$-semi-simplices. Then, semi-simplicial types come by taking $Y_{-1}$ to be a singleton.

- We do not give a positive answer to the hope of bypassing the need for coherence diagrams while defining semi-simplicial types in core homotopy type theory such as the one considered in (The Univalent Foundations Program, 2013). Even if for fixed $n$, $i$ and $j$, the equation $d_i^n \circ d_j^{n+1} = d_j^n \circ d_{i+1}^{n+1}$ for $n \ge i \ge j$ has a closed proof and hence holds by construction, it only holds up to a proof of the family of equations $d_{k'}^m \circ d_j^{n'+1} \circ d_{i'}^{n'+2} = d_{i'}^m \circ d_{j'+1}^{n'+1} \circ d_{k'+2}^{n'+2}$ when one of $n$, $i$ or $j$ is not fixed and $n \ge 1$ and the types have h-level $\ge 3$. This equation itself requires a higher-dimension coherence condition if $n \ge 2$ and the types have h-level $\ge 4$, and so on. As a consequence:

- Our definition is not applicable, in the context of core homotopy type theory, for defining semi-simplicial types with types of unbounded homotopy level.

- Our definition is applicable to the definition of semi-simplicial types over types of bounded homotopy level, say $n+2$, but this requires proving $n+1$ coherence diagrams of increasing complexity about how to equate the different ways of composing $n+2$ faces. In practice, we only considered the cases $n=0$ and $n=1$ (Section 5)†.

- However, in an idealistic situation where it is possible to have a strict equality co-existing with the default univalent equality (Voevodsky, 2011; Voevodsky, 2012b) of homotopy type theory, our definition becomes applicable for defining semi-simplicial types made of types of unbounded homotopy level (Section 4): indeed, by expressing the face equations using a strict equality, the coherence conditions hold on the fly. In particular, we fully formalized our construction in the Coq proof assistant (Coq Development Team, 2012) extended with an axiom expressing strictness of equality‡. We did not (essentially) use the **Prop** universe of Coq and the question of whether a distinct univalent equality with (necessarily) limited transport abilities can be added in a consistent way on top of the resulting type theory is open.

- As concrete examples, we give the construction of the standard semi-simplices and of the product of semi-simplicial types, as well as a sketch of the construction of the exponential of semi-simplicial types (Section 6).

Moreover, we will show in future work that the construction needs not be restricted to semi-simplicial types and that it can instead be done for simplicial types as well as for any functor over Reedy categories (with ordinal $\omega$), by first building types dependent

<footnote>† The case $n = -2$ and $n = -1$ are trivial and uninteresting.</footnote>

<footnote>‡ Coq does not natively interpret this axiom computationally. If it had, we would have gotten $d_i^n \circ d_j^{n+1} = d_j^n \circ d_{i+1}^{n+1}$ holding definitionally for $n$, $i$ and $j$ fixed.</footnote>
over the negative “skeleton” of objects (faces), and by injecting the positive morphisms (degeneracies) afterwards. Such a dependently-typed definition is constructive in the sense that, for simplicial types, whether a *n*-simplex is degenerated or not is decidable. In particular, in the case of sets, this definition will only be classically equivalent to the presheaf definition.

Note that a partial but similar generic definition of semi-simplicial types has been provided independently by Voevodsky (Voevodsky, 2012a). A comparison is done in Section 8.

## 2. Towards a dependently-typed construction of (augmented) semi-simplicial types

As initially described on the wiki of the special year on Univalent Foundations at the Institute of Advanced Study (LeFanu Lumsdaine, 2012), a (dependently-typed) semi-simplicial type is given by a family of dependent types:

Y₀ : Type
Y₁ : Πab : Y₀. Type
Y₂ : Πabc : Y₀. Πx : Y₁(a, b). Πy : Y₁(a, c). Πz : Y₁(b, c). Type
⋮

For the only sake of regularity at the start of the sequence, we shall instead consider the augmented semi-simplicial variant of this definition and add an extra type $Y_{-1}$ on which all $Y_n$'s for $n \ge 0$ depend exactly once. This change is not critical since we fall back on semi-simpliciality by taking $Y_{-1}$ to be a singleton type.

Y_{-1} : Type₁
Y₀ : Πu : Y_{-1}. Type
Y₁ : Πu : Y_{-1}. Πab : Y₀(u). Type
Y₂ : Πu : Y_{-1}. Πabc : Y₀(u). Πx : Y₁(u, a, b). Πy : Y₁(u, a, c). Πz : Y₁(u, b, c). Type
⋮

Let us fix some type universe Type₁. The first step to define the augmented $Y_n$'s generically is to rephrase them using nested Σ-types over blocks of simplices of the same dimension:
$$Y_{-1} : \mathbf{Type}_1$$

$$Y_0 : (\Sigma x : \bigwedge \{Y_{-1}\}) \to \mathbf{Type}_1$$

$$Y_1 : (\Sigma x : \bigwedge \{Y_{-1}\} \wedge \left\{ \begin{array}{l} Y_0(\pi_0^0(x)) \\ Y_0(\pi_0^0(x)) \end{array} \right\}) \to \mathbf{Type}_1$$

$$Y_2 : (\Sigma x' : \left( \Sigma x : \bigwedge \{Y_{-1}\} \wedge \left\{ \begin{array}{l} Y_0(\pi_0^0(x)) \\ Y_0(\pi_0^0(x)) \\ Y_0(\pi_0^0(x)) \end{array} \right\} \right) \wedge \left\{ \begin{array}{l} Y_1(\pi_0^0(\text{fst } x'), (\pi_0^2(\text{snd } x'), \pi_1^2(\text{snd } x')) \\ Y_1(\pi_0^0(\text{fst } x'), (\pi_0^2(\text{snd } x'), \pi_2^2(\text{snd } x')) \\ Y_1(\pi_0^0(\text{fst } x'), (\pi_1^2(\text{snd } x'), \pi_2^2(\text{snd } x')) \end{array} \right\}) \to \mathbf{Type}_1$$

$\vdots$

where $\pi_i''$ is the $i$th projection, starting from 0, out of a tuple of $n+1$ elements, while $\text{fst } x$ and $\text{snd } x$ denote the first and (dependent) second projection of the inhabitant of a $\Sigma$-type.

Let Unit denote the unit type with unit being its unique inhabitant. We go one step further in treating the base cases uniformly by ensuring that each $Y_n$ has a functional type and that nested $\Sigma$-type have Unit as common initial prefix. We thus obtain:

$$Y_{-1} : \mathbf{Unit} \to \mathbf{Type}_1$$

$$Y_0 : (\Sigma x : \mathbf{Unit} \wedge \{Y_{-1}(\mathbf{unit})\}) \to \mathbf{Type}_1$$

$$Y_1 : (\Sigma x' : (\Sigma x : \mathbf{Unit} \wedge \{Y_{-1}(\mathbf{unit})\}) \wedge \left\{ \begin{array}{l} Y_0(\mathbf{unit}, \pi_0^0(\text{snd } x')) \\ Y_0(\mathbf{unit}, \pi_0^0(\text{snd } x')) \end{array} \right\}) \to \mathbf{Type}_1$$

$$Y_2 : (\Sigma x'' : \left( \Sigma x' : (\Sigma x : \mathbf{Unit} \wedge \{Y_{-1}(\mathbf{unit})\}) \wedge \left\{ \begin{array}{l} Y_0(\mathbf{unit}, \pi_0^0(\text{snd } x'')) \\ Y_0(\mathbf{unit}, \pi_0^0(\text{snd } x'')) \\ Y_0(\mathbf{unit}, \pi_0^0(\text{snd } x'')) \end{array} \right\} \right) \wedge \left\{ \begin{array}{l} Y_1(\mathbf{unit}, \pi_0^0(\text{snd } \text{fst } x''), (\pi_0^2(\text{snd } x''), \pi_1^2(\text{snd } x'')) \\ Y_1(\mathbf{unit}, \pi_0^0(\text{snd } \text{fst } x''), (\pi_0^2(\text{snd } x''), \pi_2^2(\text{snd } x'')) \\ Y_1(\mathbf{unit}, \pi_0^0(\text{snd } \text{fst } x''), (\pi_1^2(\text{snd } x''), \pi_2^2(\text{snd } x'')) \end{array} \right\}) \to \mathbf{Type}_1$$

$\vdots$

Each block of $Y_i$'s in the type of $Y_n$, for $i < n$, is a block of iterated faces and the number of component in a block is the number of ways to choose $n-i$ elements among $n+1$ elements. For instance, the three $Y_1$ components in the definition of the type of $Y_2$ can be seen as the combination $\binom{3}{1}$ obtained by removing one element out of a triple, while the three $Y_0$ components can be seen as the combination $\binom{3}{2}$ obtained by removing two elements out of a triple. To simplify notations, let us set:

$$\mathbf{p}_2^{3,1}(x'') \triangleq (\mathbf{unit}, \pi_0^0(\text{snd } \text{fst } x''), (\pi_0^2(\text{snd } x''), \pi_1^2(\text{snd } x'')))$$

$$\mathbf{p}_1^{3,1}(x'') \triangleq (\mathbf{unit}, \pi_0^0(\text{snd } \text{fst } x''), (\pi_0^2(\text{snd } x''), \pi_2^2(\text{snd } x'')))$$

$$\mathbf{p}_0^{3,1}(x'') \triangleq (\mathbf{unit}, \pi_0^0(\text{snd } \text{fst } x''), (\pi_1^2(\text{snd } x''), \pi_2^2(\text{snd } x'')))$$
meaning that we removed 1 element respectively numbered 2, 1 and 0 out of a block of 3 elements. We can then abbreviate the block of $Y_1$'s in $Y_2$ as $\bigwedge_{i \in \binom{3}{1}} Y_2(\mathfrak{p}_i^{3,1}(x))$.

Similarly, the three $Y_0$'s in the definition of the type $Y_2$ of triangles correspond to the two iterations of the face maps in a triangle. This suggests to set:

$$ \mathfrak{p}_{12}^{3,2}(x) \triangleq (\text{unit}, \pi_0^0(\text{snd } x)) $$

$$ \mathfrak{p}_{02}^{3,2}(x) \triangleq (\text{unit}, \pi_0^0(\text{snd } x)) $$

$$ \mathfrak{p}_{01}^{3,2}(x) \triangleq (\text{unit}, \pi_0^0(\text{snd } x)) $$

meaning that we removed 2 elements respectively numbered 2 and 1, 2 and 0, and 1 and 0. We can then abbreviate the block of $Y_0$'s in $Y_2$ as $\bigwedge_{i_0 i_1 \in \binom{3}{2}} Y_1(\mathfrak{p}_{i_0 i_1}^{3,2}(x))$.

Our next step, using new such $\mathfrak{p}_{i_0 \dots i_{p-1}}^{q,p}$ abbreviations, is to rephrase the nested $\Sigma$-types involved in the definition of the domains of the $Y_n$'s into elementary $\Sigma$-types:

$$ F^{0,0} \quad \triangleq \quad \text{Unit} $$

$$ Y_{-1} \quad : \quad F^{0,0} \to \text{Type}_1 $$

$$ F^{0,1} \quad \triangleq \quad \text{Unit} $$

$$ F^{1,0}(Y_{-1}) \quad \triangleq \quad \Sigma x : F^{0,1} \cdot \bigwedge_{i \in \binom{1}{1}} Y_{-1}(\mathfrak{p}_i^{1,1}(x)) $$

$$ Y_0 \quad : \quad F^{1,0}(Y_{-1}) \to \text{Type}_1 $$

$$ F^{0,2} \quad \triangleq \quad \text{Unit} $$

$$ F^{1,1}(Y_{-1}) \quad \triangleq \quad \Sigma x : F^{0,2} \cdot \bigwedge_{i_0 i_1 \in \binom{2}{2}} Y_{-1}(\mathfrak{p}_{i_0 i_1}^{2,2}(x)) $$

$$ F^{2,0}(Y_{-1}, Y_0) \quad \triangleq \quad \Sigma x : F^{1,1}(Y_{-1}) \cdot \bigwedge_{i \in \binom{2}{1}} Y_0(\mathfrak{p}_i^{2,1}(x)) $$

$$ Y_1 \quad : \quad F^{2,0}(Y_{-1}, Y_0) \to \text{Type}_1 $$

$$ F^{0,3} \quad \triangleq \quad \text{Unit} $$

$$ F^{1,2}(Y_{-1}) \quad \triangleq \quad \Sigma x : F^{0,3} \cdot \bigwedge_{i_0 i_1 i_2 \in \binom{3}{3}} Y_{-1}(\mathfrak{p}_{i_0 i_1 i_2}^{3,3}(x)) $$

$$ F^{2,1}(Y_{-1}, Y_0) \quad \triangleq \quad \Sigma x : F^{1,2}(Y_{-1}) \cdot \bigwedge_{i_0 i_1 \in \binom{3}{2}} Y_0(\mathfrak{p}_{i_0 i_1}^{3,2}(x)) $$

$$ F^{3,0}(Y_{-1}, Y_0, Y_1) \quad \triangleq \quad \Sigma x : F^{2,1}(Y_{-1}, Y_0) \cdot \bigwedge_{i \in \binom{3}{1}} Y_1(\mathfrak{p}_i^{3,1}(x)) $$

$$ Y_2 \quad : \quad F^{3,0}(Y_{-1}, Y_0, Y_1) \to \text{Type}_1 $$

$\vdots$

which directly suggests to inductively define $F^{n,p}(Y_{-1}, Y_0, \dots, Y_{n-1})$ mutually with some $\Sigma$-type, say $sst_n$, packing the types of the sequence $Y_0, \dots, Y_{n-1}$ (see Section 4).

Each $F^{n,p}$ is a type for the collection of sub-semi-simplices of dimension less or equal than $n-2$ starting from an initial simplex of dimension $n+p-1$, where 0 is the dimension of points, 1 of lines, etc. The next difficulty is to define the family of $\mathfrak{p}_{i_0 \dots i_{p-1}}^{q,p}$ whose purpose is to select, out of the collection of sub-semi-simplices of dimension at
most $q-p-2$ of an initial $(q-1)$-semi-simplex $z$, the sub-collection of all sub-semi-simplices of the $(q-p-1)$-sub-semi-simplex obtained by applying the face maps $d_{i_{p-1}}$, ..., $d_{i_0}$ to $z$. Each $\mathbf{p}_{i_0..i_{p-1}}^{q,p}$ has type $F^{q-p,p}(Y_{-1}, ..., Y_{q-p-2}) \to F^{q-p,0}(Y_{-1}, ..., Y_{q-p-2})$ and our solution is to decompose each $\mathbf{p}_{i_0..i_{p-1}}^{q,p}$ into elementary filtering operators of type $F^{n,p}(Y_{-1}, ..., Y_{n-2}) \to F^{n,p-1}(Y_{-1}, ..., Y_{n-2})$, with $n$ being $q-p$, each of them selecting the corresponding sub-simplices obtained by removing one of the initial $n+p$ points.

Each such elementary filtering operator has to be dependent over an index $i \le n$ indicating the number of the point to remove. We write $\underline{d}_i^{n,p}$ for the elementary filtering operator that extracts, out of the collection of sub-semi-simplices of dimension at most $n-2$ of an initial $(n+p-1)$-simplex $z$, the sub-collection of those semi-simplices that are sub-semi-simplices of the face $i$ of $z$. We can then define $\mathbf{p}_{i_0..i_{p-1}}^{q,p}$ to be $\underline{d}_{i_0}^{n,0} \circ \dots \circ \underline{d}_{i_{p-1}}^{n,p-1}$ and finally take $\Sigma x : F^{n,p+1}(Y_{-1}, ..., Y_{n-1}) \wedge \bigwedge_{i_0...i_p \in \binom{n+p+1}{p+1}} Y_n(\underline{d}_{i_0}^{n,0} \dots \underline{d}_{i_p}^{n,p}(x))$ for $F^{n+1,p}(Y_{-1}, ..., Y_n)$. For instance, $F^{2,1}(Y_{-1}, Y_0)$ consists of triples of points supposed to be the points of an initial triangle (together with a $(-1)$-simplex they all depend on) and $\underline{d}_i^{2,0}$ extracts from each triple the pair of end points of side $i$ of the initial triangle (together with the same $(-1)$-simplex they all depend on). More specifically, if $u$ is a $(-1)$-simplex and $a, b$ and $c$ points over $u$, i.e. points in $Y_0(\text{unit}, u)$, then $((\text{unit}, u), (a, b, c)) \in F^{2,1}(Y_{-1}, Y_0)$ is mapped to $((\text{unit}, u), (b, c)) \in F^{2,0}(Y_{-1}, Y_0)$ by $\underline{d}_0^{2,0}$, to $((\text{unit}, u), (a, c)) \in F^{2,0}(Y_{-1}, Y_0)$ by $\underline{d}_1^{2,0}$ and to $((\text{unit}, u), (a, b)) \in F^{2,0}(Y_{-1}, Y_0)$ by $\underline{d}_2^{2,0}$.

The question is now to define such combinations.

### 3. Combinations

Let $n$ be given as well as a family of types $F^p : \text{Type}_1$, a predicate $Y : F^0 \to \text{Type}_1$ and a family of operators $\underline{d}_i^p : F^{p+1} \to F^p$, with $i \le n+p$ in $\underline{d}_i^p$. Let $p$ an integer and $x : F^p$. We can define by induction on $p$ a combination type

$$ \bigwedge_{i_0 \dots i_{p-1} \in \binom{n+p}{p}} Y(\underline{d}_{i_0}^0 \dots \underline{d}_{i_{p-1}}^{p-1}(x)) $$

denoting the Cartesian product of elements in the instantiation of $Y$ on $\underline{d}_{i_0}^0 \dots \underline{d}_{i_{p-1}}^{p-1}(x)$, over all combinations of $i_0..i_{p-1}$ satisfying $n \ge i_0 \ge \dots \ge i_{p-1} \ge 0$ (this latter ordering uniquely characterizes combinations and this is what we chose for the formalization in Coq; there is another canonical ordering obtained by expecting $n+p > i_{p-1} > \dots > i_0 \ge 0$, which incidentally is the choice we used to characterize the $\mathbf{p}_{i_0i_1}^{3,2}$ on page 6).

Let us make the additional assumption that, for all $k \ge j$, we have proofs $\underline{d}_k^p \ge j$ of the identities $\underline{d}_k^p \circ \underline{d}_j^{p+1} = \underline{d}_j^p \circ \underline{d}_{k+1}^{p+1}$. Then, we can, for each $i \le n+p$ and $x : F^{p+1}$, define by induction on $p$ a filtering operator $\bar{d}_i^{n,F,Y,d,\underline{d},p}(x)$, shortly $\bar{d}_i^p$, which extracts, out of a combination of choices of $p+1$ elements among $n+p+1$, those combinations which include the selection of the $i^{th}$ element. There are $\binom{n+p}{n}$ such choices and $i$ can be considered to be chosen first in each of these, so that $\bar{d}_i^p$ can be given the following type:
$$ \bar{d}_i^p : \bigwedge_{i_0 \dots i_p \in \binom{n+p+1}{p+1}} Y(\underline{d}_{i_0}^0 \dots \underline{d}_{i_p}^p(x)) \to \bigwedge_{i_0 \dots i_{p-1} \in \binom{n+p}{p}} Y(\underline{d}_{i_0}^0 \dots \underline{d}_{i_{p-1}}^{p-1}(\underline{d}_i^p(x))) $$

However, if $i$ can be chosen first, it does not mean that $i$ was effectively chosen first in the particular choices of $i_0 \ge \dots \ge i_p$ used for enumerating $\binom{n+p+1}{p+1}$. When $i > i_p$, $\underline{d}_{i-1 \ge i_p}$ is needed, using the induction hypothesis on $i-1$.

By $\underline{d}_i^p(\underline{d}_{k \ge j}^{p+1})$ we mean the proof of $\underline{d}_i^p \circ \underline{d}_k^{p+1} \circ \underline{d}_j^{p+2} = \underline{d}_i^p \circ \underline{d}_j^{p+1} \circ \underline{d}_{k+1}^{p+2}$ obtained by applying the congruence over $\underline{d}_i^p$ to $\underline{d}_{k \ge j}^{p+1}$. By $\underline{d}_{k \ge j}^p(\underline{d}_i^{p+2})$ we mean the specialization of $\underline{d}_{k \ge j}^p$ to $\underline{d}_i^{p+2}$ which is a proof of $\underline{d}_k^p \circ \underline{d}_j^{p+1} \circ \underline{d}_i^{p+2} = \underline{d}_j^p \circ \underline{d}_{k+1}^{p+1} \circ \underline{d}_i^{p+2}$. Then, we assume for $k \ge j \ge i$ that the following coherence property $\underline{d}_{k \ge j \ge i}^p$ of $\underline{d}$ holds, where $\cdot$ denotes the composition of equalities by transitivity:

$$ \underline{d}_{k \ge j \ge i}^p : [\underline{d}_k^p(\underline{d}_{j \ge i}^{p+1}) \cdot \underline{d}_{k \ge i}^p(\underline{d}_{j+1}^{p+2}) \cdot \underline{d}_i^p(\underline{d}_{k+1 \ge j+1}^{p+1}) = \underline{d}_{k \ge j}^p(\underline{d}_i^{p+2}) \cdot \underline{d}_j^p(\underline{d}_{k+1 \ge i}^{p+1}) \cdot \underline{d}_{j \ge i}^p(\underline{d}_{k+2}^{p+2})] $$

Note that both sides of the equation are proofs of $\underline{d}_k^p \circ \underline{d}_j^{p+1} \circ \underline{d}_i^{p+2} = \underline{d}_i^p \circ \underline{d}_{j+1}^{p+1} \circ \underline{d}_{k+2}^{p+2}$. If equality were a strict equality, uniqueness of equality proofs would hold and the assumption above would directly hold by default. However, if equality is taken to be relevant, as it is the case e.g. in homotopy type theory (The Univalent Foundations Program, 2013), there is no reason a priori it holds. This is why we take it as an assumption. Under this assumption, we can build by induction on $p$ and case analysis on $k$, $j$ and $i_p$ a proof $\underline{d}_{k \ge j}^{n,F,Y,d,d,p}(x)$, shortly $\underline{d}_{k \ge j}^p$, that the following holds for $x : F^{p+2}$ and $k \ge j$:

$$ \underline{d}_{k \ge j}^p : [\bar{d}_k^p \circ \bar{d}_j^{p+1} = \underline{d}_{k \ge j}^p \quad \bar{d}_j^p \circ \bar{d}_{k+1}^{p+1}] $$

where the notation $\underline{d}_{k \le j}^p$ means that both sides of the equation are pointwise in the same type up to transport along the equality proof $\underline{d}_{k \ge j}^p$ (pointwise here means for each $y : \bigwedge_{i_0 \dots i_{p+1} \in \binom{n+p+2}{p+2}} Y(\underline{d}_{i_0}^0 \dots \underline{d}_{i_{p+1}}^{p+1}(x))$ to which each side of the equation is applicable).

Note that $\underline{d}_{k-1 \ge j-1 \ge i_{p+1}}$ is needed when $j > i_{p+1}$ since then, all the definitions of $\bar{d}_k$, $\bar{d}_j$ and $\bar{d}_{k+1}$ reveal a use of $\underline{d}$, which, combined with an extra use of $\underline{d}$ coming from the induction hypothesis, requires $\underline{d}$.

The products over combination above can be defined as tuples. Note however that if these products were defined as functions, functional extensionality of equality would be needed to build the proof $\underline{d}$.

## 4. The initial segments of dependently-typed augmented semi-simplicial types in the presence of a strict equality

In this section, we assume strict equality to be a connective of the underlying logical theory. What happens if no strict equality is available is discussed in the next section.
We recursively define:

- the signature $sst_n$ of the $n$ first dependently-typed augmented semi-simplicial types (i.e. from the $(-1)$-semi-simplicial type to the $(n-2)$-semi-simplicial type);

- the family of signatures $F^{n,0}$ of the parameters of the $(n-1)$-semi-simplicial type: this corresponds to the type of all strict sub-semi-simplices of such a $(n-1)$-semi-simplicial type; each of $F^{n,0}$ is defined from $F^{n,p}$ which corresponds to the type of all sub-semi-simplices of dimension less than $n-2$ of a $(n+p-1)$-semi-simplex;

- the “filter-through-face” $\underline{d}_i^{n,p}$ from $F^{n,p+1}$ to $F^{n,p}$ which extracts from the collection of sub-semi-simplicial types at depth less than $n-2$ of some $r$ $(n+p)$-semi-simplex the sub-collection of sub-semi-simplicial types at depth less than $n-2$ of the $(n+p-1)$-semi-simplex which is the $i^{th}$-face of the original simplex ($i$ ranges from 0 to $n+p$);

- an identity over filters, reminiscent of the face identity, asserting $\underline{d}_k^{n,p} \circ \underline{d}_j^{n,p+1} = \underline{d}_j^{n,p} \circ \underline{d}_{k+1}^{n,p+1}$ for $k \ge j$.

Below, we generally let $i$ range over values below $n+p$. We sometimes omit the argument $X$ of $\underline{d}$, $\underline{d}$.

$$
\begin{align*}
sst_n & : \text{Type}_2 \\
sst_0 & \triangleq \text{Unit} \\
sst_{n+1} & \triangleq \Sigma X : sst_n.(F^{n,0}(X) \to \text{Type}_1) \\
F^{n,p} & (X : sst_n) : \text{Type}_1 \\
F^{0,p} & \underline{\text{unit}} : \underline{\text{Unit}} \\
F^{n+1,p} & (X, Y) \triangleq \Sigma x : F^{n,p+1}(X) \\
& \quad \wedge_{i_0 \dots i_p \in \binom{n+p+1}{p+1}} Y(\underline{d}_{i_0}^{n,0} \dots \underline{d}_{i_p}^{n,p}(x)) \\
\underline{d}_i^{n,p} & (X : sst_n)(x : F^{n,p+1}(X)) : F^{n,p}(X) \\
\underline{d}_i^{0,p} & \underline{\text{unit}} : \underline{\text{unit}} \\
\underline{d}_i^{n+1,p} & (X, Y)(x, y) \triangleq (\underline{d}_i^{n,p+1}(x), \bar{\underline{d}}_i^{n,F^n,Y,\underline{d}^n,\underline{d}^n,p+1}(x)(y)) \\
\underline{d}_k^{n,p} & (X : sst_n)(x : F^{n,p+2}(X)) : \underline{d}_k^{n,p} \underline{d}_j^{n,p+1}(x) = \underline{d}_j^{n,p} \underline{d}_{k+1}^{n,p+1}(x) \\
\underline{d}_k^{0,p} & \underline{\text{unit}} : \underline{\text{refl}} \\
\underline{d}_k^{n+1,p} & (X, Y)(x, y) \triangleq (\underline{d}_k^{n,p+1}(x), \bar{\underline{d}}_{k \ge j}^{n,F^n,Y,\underline{d}^n,\underline{d}^n,p+1}(x)(y))
\end{align*}
$$

where, in the last line,

$$
\begin{align*}
\underline{d}^n & : [\underline{d}_k^p (\underline{d}_{j \ge i}^{p+1})(x) \cdot \underline{d}_{k \ge i}^p (\underline{d}_{j+1}^{p+2})(x) \cdot \underline{d}_i^p (\underline{d}_{k+1 \ge j+1}^{p+1})(x) \\
& = \underline{d}^p (\underline{d}_i^{p+2})(x) \cdot \underline{d}_j^p (\underline{d}_{k+1 \ge i}^{p+1})(x) \cdot \underline{d}^p (\underline{d}_{k \ge j}^{p+2})(x)]
\end{align*}
$$

comes as a consequence of the strictness of the equality.

The definition above has been fully formalized in Coq, using an equality that satisfies uniqueness of reflexivity proofs. The faces identities for specific values of $n$, $i$ and $j$ would hold definitionally if Coq had supported a definitional form of uniqueness of reflexivity proofs (e.g. by providing Streicher's axiom K with its reduction rule).
5. The initial segments of a dependently-typed augmented semi-simplicial
types in the absence of a strict equality

We now place ourselves in a context where equality is not provably strict. Then, *n* extra coherence conditions have to be proved to support the construction of augmented semi-simplicial types with types at h-level *n* + 2.

The construction made in Section 4 works directly for types at h-level 2, since then,
equality between elements of such types is strict.

To construct (augmented) semi-simplicial types with types at h-level 3, we need to
prove an extra coherence condition, and for that purpose, we assume given a proof
$\overline{\equiv}^{n,F,Y,d,d,d,p}$, shortly $\overline{\equiv}_p$
$\overline{d}_{k \ge j \ge i}$, of the following coherence property over combinations:

$$
\overline{\equiv}_p \overline{d}_{k \ge j \ge i} : [ \overline{d}_k^p (\overline{d}_{j \ge i}^{p+1}) \cdot \overline{d}_{k \ge i}^p (\overline{d}_{j+1}^{p+2}) \cdot \overline{d}_i^p (\overline{d}_{k+1 \ge j+1}^{p+1}) ] = \overline{\equiv}_p \overline{d}_{k \ge j}^p (\overline{d}_i^{p+2}) \cdot \overline{d}_j^p (\overline{d}_{k+1 \ge i}^{p+1}) \cdot \overline{d}_{j \ge i}^p (\overline{d}_{k+2}^{p+2})
$$

where the $\overline{d}_i^p(\overline{d}_{k \ge j}^{p+1})$ are proofs of $\overline{d}_i^p \circ \overline{d}_k^{p+1} \circ \overline{d}_j^{p+2} = \overline{d}_i^p(\overline{d}_{k \ge j}^{p+1}) \overline{d}_i^p \circ \overline{d}_j^{p+1} \circ \overline{d}_{k+1}^{p+2}$ and the $\overline{d}_{k \ge j}^{p+1}(\overline{d}_i^p)$ are proofs of $\overline{d}_i^p \circ \overline{d}_j^{p+1} \circ \overline{d}_i^{p+2} = \overline{d}_{k \ge j}^p(\overline{d}_i^{p+2}) \overline{d}_j^p \circ \overline{d}_{k+1}^{p+1} \circ \overline{d}_i^{p+2}$. Note that the left-hand side is then a proof of

$$
\overline{d}_k^p \circ \overline{d}_j^{p+1} \circ \overline{d}_i^{p+2} = \overline{d}_k^p(\overline{d}_{j \ge i}^{p+1}) \cdot \overline{d}_k^p(\overline{d}_{j+1}^{p+2}) \cdot \overline{d}_i^p(\overline{d}_{k+1 \ge j+1}^{p+1}) \quad \overline{d}_i^p \circ \overline{d}_{j+1}^{p+1} \circ \overline{d}_{k+2}^{p+2}
$$

while the right-hand side is a proof of

$$
\overline{d}_k^p \circ \overline{d}_j^{p+1} \circ \overline{d}_i^{p+2} = \overline{d}_{k \ge j}^p (\overline{d}_i^{p+2}) \cdot \overline{d}_j^p (\overline{d}_{k+1 \ge i}^{p+1}) \cdot \overline{d}_{j \ge i}^p (\overline{d}_{k+2}^{p+2}) \quad \overline{d}_i^p \circ \overline{d}_{j+1}^{p+1} \circ \overline{d}_{k+2}^{p+2}
$$

so that the equality is correct only up to pointwise transport along $\overline{d}_{k \ge j \ge i}^p$.

We can now define dependently-typed (augmented) semi-simplicial types at h-level 3
by inductively proving the following extra property mutually with the definition of sst<sub>n</sub>,
F<sup>n,p</sup>, d<sub>i</sub><sup>n,p</sup> and d<sub>k≥j</sub><sup>n,p</sup>:

$$
\begin{align*}
\overline{d}_{k \ge j \ge i}^{m,p} (X : \mathrm{sst}_n)(x : F^{n,p+3}(X)) & : \quad \overline{d}_k^p(\overline{d}_{j \ge i}^{p+1})(x) \cdot \overline{d}_{k \ge i}^p(\overline{d}_{j+1}^{p+2})(x) \cdot \overline{d}_i^p(\overline{d}_{k+1 \ge j+1}^{p+1})(x) \\
& = \\
& \qquad \overline{d}_{k \ge j}^p(\overline{d}_i^{p+2})(x) \cdot \overline{d}_j^p(\overline{d}_{k+1 \ge i}^{p+1})(x) \cdot \overline{d}_{j \ge i}^p(\overline{d}_{k+2}^{p+2})(x)
\end{align*}
$$

$$
\overline{d}_{k \ge j \ge i}^{0,p} \quad \text{unit unit} \quad : \quad \text{refl}
$$

$$
\overline{d}_{k \ge j \ge i}^{n+1,p} (X, Y) (x, y) : \left( \overline{d}_{k \ge j \ge i}^{n,p+1} (x), \overline{d}_{k \ge j \ge i}^{\equiv n, F^n, Y, d^n, d^n, d^n, p+1} (x)(y) \right)
$$

We suspect that the proof of $\overline{\equiv}$ requires to prove a coherence diagram involving the
commutation of $\overline{d}$. With types at h-level 3, this extra coherence diagram would hold by
definition of h-level 3.

We suspect that *n* such new extra coherence diagrams have to be proved each time
we want the formalization to be applicable to types of h-level *n* + 2. In particular, using
non-strict equality, the dependently-typed construction of (augmented) semi-simplicial
types cannot be done over a family of types whose h-levels are not bounded.
# 6. Examples

## 6.1. Standard semi-simplicial types

In the standard (augmented) semi-simplicial type $\Delta[m]$, the type of $(-1)$-simplices is empty and the type of 0-simplices (points) is the interval $[0, m]$. Then, the set of $n$-simplices over $n+1$ ordered points contains a (unique) simplex if and only if the points it is based on are ordered along the numerical order.

We can then define the initial segments of the standard semi-simplicial type $\Delta[m]$ mutually with auxiliary functions as follows:

$$ 
\begin{align*}
\Delta[m](n) & : sst_n \\
\Delta[m](0) & : \triangleq \text{unit} \\
\Delta[m](1) & : \triangleq (\text{unit}, \lambda\text{unit}\text.{\text{Unit}}) \\
\Delta[m](2) & : \triangleq ((\text{unit}, \lambda\text{unit}\text.{\text{Unit}}), \lambda x.[0, m]) \\
\Delta[m](n+3) & : \triangleq (\Delta[m](n+2), \lambda x.\text{mklin}^{n+2}(x))
\end{align*}
$$

$$ 
\begin{align*}
\text{mklin}^n & (x : F^{n,0}(\Delta[m](n))) : \quad \text{Type}_1 \\
\text{mklin}^0 & x : \quad \triangleq \text{Unit} \\
\text{mklin}^1 & x : \quad \triangleq \text{Unit} \\
\text{mklin}^2 & (x, y) : \quad \triangleq \bar{d}_1^{1,0}(y) < \bar{d}_0^{1,0}(y) \\
\text{mklin}^{n+3} & (x, y) : \quad \triangleq \text{mklt}^{n+2}(\underline{d}_1^{n+2,0}(x))(\underline{d}_0^{n+2,0}(x)) \\
& \phantom{\triangleq \text{mklt}^{n+2}(} \wedge \text{mklin}^{n+2}(\underline{d}_0^{n+2,0}(x))
\end{align*}
$$

$$ 
\begin{align*}
\text{mklt}^n & (x_1 : F^{n,0}(\Delta[m](n))) : \quad \text{Type}_1 \\
\text{mklt}^0 & (x_2 : F^{n,0}(\Delta[m](n))) : \quad \triangleq \text{Unit} \\
\text{mklt}^1 & x_1 x_2 : \quad \triangleq \text{Unit} \\
\text{mklt}^2 & (x_1, y_1) (x_2, y_2) : \quad \triangleq \bar{d}_1^{1,0}(y_1) < \bar{d}_1^{1,0}(y_2) \\
\text{mklt}^{n+3} & (x_1, y_1) (x_2, y_2) : \quad \triangleq \text{mklt}^{n+2}(\underline{d}_1^{n+2,0}(x_1))(\underline{d}_1^{n+2,0}(x_2))
\end{align*}
$$

Some $n$-simplex being given, the points the $n$-simplex is composed of can be retrieved by applying each of the $n+1$ iterated faces of the form $d_1^1 \circ \dots \circ d_1^i \circ d_0^{i+1} \circ \dots \circ d_0^n$, where $i$ ranges between 0 and $n$. This translates over the collection $x$ of subsimplices of some $n$-simplex as similar compositions of $d$, ending with $\bar{d}$. Calling this function $\phi_i$, the purpose of `mklin` is to build the conjunction of constraints $\phi_{i+1}(x) < \phi_i(x)$. The function `mklt` comes as a helper. For $\underline{d}_0(x)$ and $\underline{d}_1(x)$ produced by `mklin`, `mklt` recursively applies $\underline{d}_1$ to them, ending with $\bar{d}_1$, eventually producing a point.

In the construction, conjunctions of inequalities need to be proof-irrelevant. This can easily be done by defining `<` by cases so that it returns either `Unit` or the empty type, `Empty`.
## 6.2. Product

We consider how to build the product of initial segments of (augmented) semi-simplicial types. To define the product of two semi-simplicial types, we need to prove some equalities relating the $\bar{d}$'s and the projections. For $X_1$ and $X_2$ of type $sst_n$, we define $X_1 \times X_2$ of type $sst_n$ by induction on $n$ as follows, where we sometimes omit the arguments $X_1$ and $X_2$:

$$ (X_1 \times X_2)_n \quad : \quad sst_n \\ (\text{unit} \times \text{unit})_0 \quad \triangleq \quad \text{unit} \\ ((X_1, Y_1) \times (X_2, Y_2))_{n+1} \quad \triangleq \quad ((X_1 \times X_2)_n, \lambda x : F^{n,0}((X_1 \times X_2)_n) \wedge \left\{ \begin{array}{l} Y_1(\text{proj}_{1,0}^{n,0}(X_1, X_2)(x)) \\ Y_2(\text{proj}_{2,0}^{n,0}(X_1, X_2)(x)) \end{array} \right\} ) $$

$$ \text{proj}_1^{n,p} \quad (X_1 : sst_n) (X_2 : sst_n) \quad : \quad F^{n,p}(X_1) \\ (x : F^{n,p}((X_1 \times X_2)_n)) \quad \triangleq \quad \text{unit} $$

$$ \text{proj}_1^{n+1,p} \quad (X_1, Y_1) (X_2, Y_2) (x, y) \quad \triangleq \quad (\text{proj}_1^{n,p+1}(x), \text{map}^{n,p}(\text{proj}_1^n, \lambda x.\pi_1, \underline{h}_1^n)(x)(y)) $$

$$ \text{proj}_2^{n,p} \quad (X_1 : sst_n) (X_2 : sst_n) \quad : \quad F^{n,p}(X_2) \\ (x : F^{n,p}((X_1 \times X_2)_n)) \quad \triangleq \quad \text{unit} $$

$$ \text{proj}_2^{n+1,p} \quad (X_1, Y_1) (X_2, Y_2) (x, y) \quad \triangleq \quad (\text{proj}_2^{n,p+1}(x), \text{map}^{n,p}(\text{proj}_2^n, \lambda x.\pi_2, \underline{h}_2^n)(x)(y)) $$

$$ \underline{h}_{1,i}^{n,p} \quad (X_1 : sst_n) (X_2 : sst_n) \quad : \quad \text{proj}_1^{n,p}(\underline{d}_i^{n,p}((X_1 \times X_2)_n)(x)) \\ (x : F^{n,p+1}((X_1 \times X_2)_n)) \quad = \quad \underline{d}_i^{n,p}(X_1)(\text{proj}_1^{n,p+1}(x)) $$

$$ \underline{h}_{1,i}^{0,p} \quad \text{unit} \quad \text{unit} \quad \text{unit} \quad : \quad \text{refl} \\ \underline{h}_{1,i}^{n+1,p} \quad (X_1, Y_1) (X_2, Y_2) (x, y) \quad : \quad (\underline{h}_{1,i}^{n,p+1}(x), \overline{h}_{1,i}^{n,p}(\text{proj}_1^{n,0}, \lambda x.\pi_1)(x)(y)) $$

$$ \underline{h}_{2,i}^{n,p} \quad (X_1 : sst_n) (X_2 : sst_n) \quad : \quad \text{proj}_2^{n,p}(\underline{d}_i^{n,p}((X_1 \times X_2)_n)(x)) \\ (x : F^{n,p+1}((X_1 \times X_2)_n)) \quad = \quad \underline{d}_i^{n,p}(X_2)(\text{proj}_2^{n,p+1}(x)) $$

$$ \underline{h}_{2,i}^{0,p} \quad \text{unit} \quad \text{unit} \quad \text{unit} \quad : \quad \text{refl} \\ \underline{h}_{2,i}^{n+1,p} \quad (X_1, Y_1) (X_2, Y_2) (x, y) \quad : \quad (\underline{h}_{2,i}^{n,p+1}(x), \overline{h}_{2,i}^{n,p}(\text{proj}_2^{n,0}, \lambda x.\pi_2)(x)(y)) $$

where $\text{map}^{n,F,G,Y,Z,d,e}(f,g,\underline{h})$, shortly $\text{map}(f,g,\underline{h})$, is defined for $n, F^p : \text{Type}, G^p : \text{Type}, Y : F^0 \to \text{Type}, Z : G^0 \to \text{Type}, \underline{d}_i^p : F^{p+1} \to F^p, \underline{e}_i^p : G^{p+1} \to G^p, f^p : F^p \to G^p, g : \Pi x : F^0, Y(x) \to Z(f^0(x))$ and $\underline{h}_i^p : \Pi x : F^{p+1}, f^p(\underline{d}_i^p(x)) = \underline{e}_i^p(f^{p+1}(x))$. For $p$ being given and $x$ of type $F^{p+1}$, it has the following type:

$$ \text{map}^{n,p}(f,g,\underline{h})(x) \quad : \quad \bigwedge_{i_0 \dots i_p \in \binom{n+p+1}{p+1}} Y(\underline{d}_{i_0}^{n,0} \dots \underline{d}_{i_p}^{n,p}(x)) \\ \to \bigwedge_{i_0 \dots i_p \in \binom{n+p+1}{p+1}} Z(\underline{e}_{i_0}^{n,0} \dots \underline{e}_{i_p}^{n,p}(f^p(x))) $$
and it satisfies the property:

$$ \begin{aligned} \overline{h_i^p}(f,g)(x)(y) & : \mathbf{map}^{n,p}(f,g,\underline{h})(\underline{d}_i^p(x))(\overline{d}_i^p(x)(y)) \\ & = \underline{h}^{p+1}(i)(x) \quad \overline{e}_i^p(\underline{e}_i^p(f^p(x)))(\mathbf{map}^{n,p}(f,g,\underline{h})(x)(y)) \end{aligned} $$

This latter property is provable under the assumption:

$$ f^p(\underline{d}_i^p) \cdot \underline{h}_i^p(\underline{d}_{k+1}^{p+1}) \cdot \underline{e}_i^p(\underline{h}_{k+1}^{p+1}) = \underline{h}_k^p(\underline{d}_i) \cdot \underline{e}_k^p(\underline{h}_i^{p+1}) \cdot \underline{b}_{ik}(f^p) $$

This latter property holds if equality is taken to be strict. Otherwise, it is expected to be provable by recursively relying on higher-dimension equalities, the number of whose being bounded by $n$ and by the h-levels of $Y$ and $Z$. In particular, we do not see how this property could be solved uniformly at all $n$ without having a uniform bound on the h-levels of $Y$ and $Z$ all over the construction.

### 6.3. Exponential

We sketch the definition of the exponential $X_2^{X_1}$ of the finite parts $X_1, X_2 : \mathbf{sst}_n$ of two (augmented) semi-simplicial types. Interestingly, because the dependently-typed construction of semi-simplicial types carries straightaway the whole structure of sub-semi-simplices of a semi-simplex, this structure does not have to be explicitly added as it is the case with the presheaf definition.

$$ \begin{array}{lclcl} (X_2^{X_1})_n & : & \mathbf{sst}_n & & \\ (\mathbf{unit}^{\mathbf{unit}})_0 & \triangleq & \mathbf{unit} & & \\ ((X_2, Y_2)^{(X_1, Y_1)})_{n+1} & \triangleq & ((X_2^{X_1})_n, \lambda f : F^{n,0}((X_2^{X_1})_n), \Pi x : F^{n,0}(X_1), & \\ & & Y_1(x) \to Y_2(\underline{\mathbf{apply}}^{n,0} f x)) & & \end{array} $$

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \underline{\mathbf{apply}}^{n,p} & (X_1 : \mathbf{sst}_n) & (X_2 : \mathbf{sst}_n) & & \\ \underline{\mathbf{apply}}^{n,p} & (f : F^{n,p}((X_2^{X_1})_n)) & : & F^{n,p}(X_2) \\ & (x : F^{n,p}(X_1)) & & \\ \underline{\mathbf{apply}}^{0,p} & \mathbf{unit} \ \mathbf{unit} \ \mathbf{unit} \ \mathbf{unit} & \triangleq & \mathbf{unit} \\ \underline{\mathbf{apply}}^{n+1,p} & (X_1, Y_1) & (X_2, Y_2) & (f,g) & (x,y) & \triangleq & (\underline{\mathbf{apply}}^{n,p+1} f x, \underline{\mathbf{apply}}^{n,p} f g x y) \\ & (X_1 : \mathbf{sst}_n) & (X_2 : \mathbf{sst}_n) & & \\ \underline{\mathbf{apply}}^{n,p} & (f : F^{n,p+1}((X_2^{X_1})_n)) & : & \underline{\mathbf{apply}}^{n,p} (\underline{d}_i^{n,p}(f)) (\underline{d}_i^{n,p}(x)) \\ & (x : F^{n,p+1}(X_1)) & & = \underline{d}_i^{n,p}(\underline{\mathbf{apply}}^{n,p+1} f x) \\ \underline{\mathbf{apply}}^{0,p} & \mathbf{unit} \ \mathbf{unit} \ \mathbf{unit} \ \mathbf{unit} & \triangleq & \mathbf{refl} \\ \underline{\mathbf{apply}}^{n+1,p} & (X_1, Y_1) & (X_2, Y_2) & (f,g) & (x,y) & \triangleq & (\underline{\mathbf{apply}}^{n,p+1} f x, \underline{\mathbf{apply}}^{n,p} f g x y) \end{array} $$
where, for

$$
\begin{align*}
f: & F^{n,p+1}((X_2^{X_1})_n) \\
g: & \bigwedge_{i_0 \dots i_p \in \binom{n+p+1}{p+1}} \Pi x : F^{n,0}(X_1) \cdot Y_1(x) \to Y_2(\underline{\text{apply}}^{n,0} (\underline{d}_{i_0}^{n,0} \dots \underline{d}_{i_p}^{n,p}(f)) x) \\
x: & F^{n,p}(X_1) \\
y: & \bigwedge_{i_0 \dots i_p \in \binom{n+p+1}{p+1}} Y_1(\underline{d}_{i_0}^{n,0} \dots \underline{d}_{i_p}^{n,p}(x))
\end{align*}
$$

we define

$$
\overline{\text{apply}}^{n,p}(f,g,x,y) : \bigwedge_{i_0 \dots i_p \in \binom{n+p+1}{p+1}} Y_2(\underline{d}_{i_0}^{n,0} \dots \underline{d}_{i_p}^{n,p}(x))
$$

what requires the auxiliary result **apply** that **apply** commutes with **d**, which itself requires
a proof **apply** that **apply** commutes with **d**.

7. Full dependently-typed construction of augmented semi-simplicial types

From the initial segments of the dependently-typed construction of a augmented semi-
simplicial type, it is easy to build a full augmented semi-simplicial type. This can be
defined as

$$
\mathrm{SST} \triangleq \mathrm{SST}_0(\mathrm{unit})
$$

where $\mathrm{SST}_n(X) : \mathrm{Type}_1$ for $X : \mathrm{sst}_n$ is defined coinductively in type theory as “the trailing sequence of $X_p$ for $p \ge n$ with initial prefix $X''$. The coinductive type $\mathrm{SST}_n(X)$ is defined by its destructors:

$$
\begin{array}{c@{\hspace{2em}}c}
\begin{array}{c}
S : \mathrm{SST}_n(X) \\
\hline
\text{this } S : F^{n,0}(X) \to \mathrm{Type}_1
\end{array}
&
\begin{array}{c}
S : \mathrm{SST}_n(X) \\
\hline
\text{next } S : \mathrm{SST}_{n+1}(X, \text{this } S)
\end{array}
\end{array}
$$

In particular, if *S* is an augmented semi-simplicial type, then, its underlying *p*-semi-
simplicial type *next*<sub>*p*</sub> and its underlying *p*-initial prefix *this*<sub>*p*</sub> *S* are given by iterating
*nextfrom* where, assuming *X* to be an initial semi-simplicial prefix of type *sst*<sub>*n*</sub>, the
operator *nextfrom*(*X*, *S*) ≜ ((*X*, this *S*), (next *S*)) extends the *n*-th decomposition of *S* :
SST into (*X*, *S*) with *X* : *sst*<sub>*n*</sub> and *S* : *SST*<sub>*n*</sub>(*X*) to its *n* + 1-th decomposition into some
(*X*′, *S*′) with *X*′ : *sst*<sub>*n*+1</sub> and *S*′ : *SST*<sub>*n*+1</sub>(*X*′):

$$
\begin{align*}
\text{next}_n S & : \quad sst_n \\
\triangleq & \quad \text{fst} (\text{nextfrom}^n (\text{unit}, S))
\end{align*}
$$

$$
\begin{align*}
\text{this}_n S & : \quad F^{n,0}(\text{next}_n S) \to \text{Type}_1 \\
\triangleq & \quad \text{this} (\text{snd} (\text{nextfrom}^n (\text{unit}, S)))
\end{align*}
$$

The total space of each this<sub>n</sub>S (what corresponds to the type X<sub>n-1</sub> of (n - 1)-semi-
simplices in the introduction) is:

$$
\mathcal{T}_n(S) \triangleq \Sigma x : F^{n,0}(\mathrm{next}_n(S)).\mathrm{this}_n(S)(x).
$$
Its faces $d_i^n$, from $\mathcal{T}_{n+1}(S)$ to $\mathcal{T}_n(S)$, are defined by:

$$d_i^n((x, y), z) \triangleq (\underline{d}_i^{n,0}(x), \bar{d}_i^{n,0}(x)(y)).$$

They commute thanks to the properties $\underline{d}$ and $\bar{\underline{d}}$.

**Remarks:** As an alternative to the coinductive construction of SST, we could also consider the directed families of $X_n : sst_n$, i.e. the families $(X_n)_{n \in \mathbb{N}}$ such that $fst X_{n+1} = X_n$. Also, the type of (non augmented) semi-simplicial types can be defined to be $SST_1(\text{unit}, \lambda\text{unit}.\text{Unit})$.

## 8. Voevodsky's dependently-typed formalization of semi-simplicial types

Voevodsky started a formalization of dependently-typed (non augmented) semi-simplicial types in the Coq proof assistant (Voevodsky, 2012a). The idea is similar to ours. Using our notations, it starts as follows§ where $[j] \leftrightarrow [k]$ denotes the set of injections from the interval $[j]$ of the first $j+1$ natural numbers to the $[k]$ such interval:

$$
\begin{align*}
sst_n & : & \text{Type}_2 \\
sst_0 & \triangleq & \text{Type}_1 \\
sst_{n+1} & \triangleq & \Sigma X : sst_n \cdot F^{n,n+1}(X) \to \text{Type}_1 \\
F^{n,j} & (X : sst_n) & : & \text{Type}_1 \\
F^{0,j} & X & \triangleq & [j] \to X \\
F^{n+1,j} & (X, Y) & \triangleq & \Sigma x : F^{n,j}(X) \cdot \Pi s \in ([n+1] \leftrightarrow [j]) \cdot Y(\underline{d}_s^{n,n+1,j}(x)) \\
\underline{d}_{s:\![j]}^{n,j,k} & (X : sst_n) & (x : F^{n,k}(X)) : & F^{n,j}(X) \\
\underline{d}_s^{0,j,k} & X & \triangleq & x \circ s \\
\underline{d}_s^{n+1,j,k} & (X, Y) & (x, y) & \triangleq (\underline{d}_s^{n,j,k}(X)(x), \lambda s' \in ([n+1] \leftrightarrow [j]) \cdot y(s \circ s'))
\end{align*}
$$

It remains to prove $\underline{d}_{s \circ s'}^{n,n+1,k}(x) = \underline{d}_{s'}^{n,n+1,j}(\underline{d}_s^{n,j,k}(x))$ to justify the last line of the definition. This is suspected to hold by Voevodsky under the assumption that the type theory supports some extensional form of “definitional equality”. This basically reduces to supporting (computable) strict equality, and, indeed, based on our work, everything suggests that the equation holds when stated using strict equality.

The difference between Voevodsky's construction and ours reflects different views over the underlying structure of face maps.

Voevodsky's construction relies on the categorical structure of face maps, namely on composition and associativity of composition. Contrastingly, our construction relies on the combinatorial structure of them, namely their factorization into atomic faces up to face identities.

<footnote>§ We slightly simplified the formalization: in the original Coq file, both $F$, called *sks*, and $d$, called *restr*, had an extra argument $i \le n$, reminiscent of some possible need for well-founded induction but which happened not to be used (i.e. $i$ only needs to be $n$ in practice). We dropped this argument.</footnote>
In Voevodsky’s construction, the face identities are proved within the (syntactic) category of faces as part of the proof of associativity of composition. In our construction, associativity of faces comes for free but the proofs of face identities surfaces within the (semantical) construction of semi-simplicial types.

There is a secondary orthogonal issue. When the collections of $j$-sub-semi-simplices are represented using a $\Pi$-type, as in the definition of $F^{n+1,j}$ above, functional extensionality is needed, here to prove $\underline{d}_{sos'}^{n,n+1,k}(x) = \underline{d}_{s'}^{m,n+1,j}(\underline{d}_s^{n,j,k}(x))$. Contrastingly, functional extensionality of equality is not needed when the collections of sub-semi-simplices of some dimension are represented by tuples.

## References

* Coq Development Team, T. (2012). *The Coq Reference Manual, version 8.4*. Distributed electronically at http://coq.inria.fr/doc.

* Friedman, G. (2012). Survey article: An elementary illustrated introduction to simplicial sets.

* LeFanu Lumsdaine, P. (2012). Semi-simplicial types. Online at http://uf-ias-2012.wikispaces.com/Semi-simplicial+types.

* The Univalent Foundations Program, IAS. (2013). Homotopy type theory: Univalent foundations of mathematics. Technical report, Institute for Advanced Study.

* Voevodsky, V. (2011). Univalent foundations of mathematics. In *Logic, Language, Information and Computation*, volume 6642 of *Lecture Notes in Computer Science*, page 4, Berlin - Heidelberg. Springer.

* Voevodsky, V. (2012a). Semi-simplicial types. Online at http://uf-ias-2012.wikispaces.com/Semi-simplicial+types.

* Voevodsky, V. (2012b). Univalent foundations repository. Ongoing Coq development, https://github.com/vladimirias/Foundations.