nLab semi-simplicial type

Idea

The notion in the corresponding internal logic (i.e. in dependent type theory) of a semi-simplicial object in a locally cartesian closed (infinity,1)-category.

Similarly to semi-simplicial sets, there are typically two approaches that one can take to defining semi-simplicial types in dependent type theory:

• One can define fibered semi-simplicial types as an (infinity,1)-presheaf on the category $\Delta_+$ of finite inhabited ordinals and injections via synthetic $(\infty,1)$-category theory.

• One can define indexed semi-simplicial types as a family of families by iterating the correspondence between fibrations and families based on “iterated dependencies”.

None of these approaches are currently possible in plain dependent type theory or homotopy type theory due to the issue of handling infinity many data in a finitary manner, whether for the iterated families of semi-simplicial types or the coherence laws of $(\infty,1)$-categories. Instead, defining semi-simplicial types requires the extension of dependent type theory with additional features, such as

• modalities for synthetic (infinity,1)-category theory (e.g. simplicial type theory, triangulated type theory),

• other levels / non-fibrant types / infinitary record types (e.g. two-level type theory, type theory with shapes, Homotopy Type System),

• internal parametricity / modal parametricity (e.g. some cubical type theory, displayed type theory, cohesive type theory with sufficient cohesion)

Historically, the “iterated dependency” approach to semi-simplicial sets has given dependent type theorists a candidate approach for tackling coherence issues in dependent type theory. With simplicial sets, it’s hard to see how one might tackle or avoid them. (Comparing it to the semi-simplicial approach, one requires degeneracy maps and equations between them, which lets loose the spectre of coherence again.) Furthermore, reasoning about Kan simplicial sets seems to insist on classical logic. For example, the classical result stating the homotopy equivalence of fibers of a Kan fibration cannot be proved constructively (pdf). In homotopy-theoretic terms, this is because $\Delta_+$ is a direct category, while the simplex category $\Delta$ is not.

Definition

Fibered semi-simplicial types

We work in a dependent type theory which supports synthetic $(\infty,1)$-category theory, such as simplicial type theory or triangulated type theory.

With the op modality $(-)^\op$, the directed univalent type universe $\mathcal{S}$, and the $(\infty,1)$-subcategory $\Delta_+ \subseteq \mathcal{S}$ of finite inhabited ordinals and injections, a semi-simplicial type is simply a function $X:\Delta_+^op \to \mathcal{S}$, which is provably an $(\infty,1)$-presheaf by the directed structure identity principle on $(\infty,1)$-presheaf $(\infty,1)$-categories.

Indexed semi-simplicial types

To illustrate the idea of indexed semi-simplicial types as families of families of $n$-semi-simplices, let us consider the finite-dimensional parts of such an indexed semi-simplicial type:

Let $U$ be a type universe. Then,

• A $U$-small indexed 0-semi-simplicial type is just a $U$-small type $X_0:U$.

• A $U$-small indexed 1-semi-simplicial type is $U$-small indexed 0-semi-simplicial type $X_0$ with a family of $U$-small types

  $$x_0:X_0, x_1:X_0 \vdash X_1(x_0, x_1):U$$

• A $U$-small indexed 2-semi-simplicial type is a $U$-small indexed 1-semi-simplicial type $(X_0, X_1)$ with a family of $U$-small types

  $$x:X_0, x_1:X_0, x_2:X_0, x_{0, 1}:X_1(x_0, x_1), x_{1, 2}:X_1(x_1, x_2), x_{0, 2}:X_1(x_0, x_2) \vdash X_2(x_0, x_1, x_2, x_{0, 1}, x_{1, 2}, x_{0, 2}):U$$

  representing triangular configurations from $X_0$ and $X_1$.

• A $U$-small indexed 3-semi-simplicial type is a $U$-small indexed 2-semi-simplicial type $(X_0, X_1, X_2)$ with a family of $U$-small types

  $$\begin{array}{l} x:X_0, x_1:X_0, x_2:X_0, x_3:X_0, \\ x_{0, 1}:X_1(x_0, x_1), x_{1, 2}:X_1(x_1, x_2), x_{2, 3}:X_1(x_2, x_3), \\ x_{0, 2}:X_1(x_0, x_2), x_{1, 3}:X_1(x_1, x_3), x_{0, 3}:X_1(x_0, x_3), \\ x_{0, 1, 2}:X_2(x_0, x_1, x_2, x_{0, 1}, x_{1, 2}, x_{0, 2}), x_{0, 1, 3}:X_2(x_0, x_1, x_3, x_{0, 1}, x_{1, 3}, x_{0, 3}), \\ x_{0, 2, 3}:X_2(x_0, x_2, x_3, x_{0, 2}, x_{2, 3}, x_{0, 3}), x_{1, 2, 3}:X_2(x_1, x_2, x_3, x_{1, 2}, x_{2, 3}, x_{1, 3}), \\ \vdash X_2(x_0, x_1, x_2, x_3, x_{0, 1}, x_{1, 2}, x_{2, 3}, x_{0, 2}, x_{1, 3}, x_{0, 3}, x_{0, 1, 2}, x_{0, 1, 3}, x_{0, 2, 3}, x_{1, 2, 3}):U \end{array}$$

  representing tetrahedral configurations from $X_0$, $X_1$ and $X_2$.

And so on. Then a $U$-small indexed semi-simplicial type (i.e. indexed infinity-semi-simplicial types) should be a type that is an indexed $n$-semi-simplicial type for all $n$.

Using bridge types

Suppose that the dependent type theory has unary bridge types $(\mathrm{Br}_A(x))_{x:A}$. Then given a type universe $U$, the type of $U$-small indexed semi-simplicial types $U^{\Delta_{+}^\op}$ is a displayed coinductive type cogenerated by

• a function $Z^+:U^{\Delta_{+}^\op} \to U$ and

• a dependent function

  $$S^+:\prod_{X:U^{\Delta_{+}^\op}} Z^+(X) \to \mathrm{Br}_{U^{\Delta_{+}^\op}}(X)$$

An indexed semi-simplicial type is simply an element of $U^{\Delta_{+}^\op}$, and the iterated dependencies are given by iterated bridge types. See e.g. Kolomatskaia 2022, Kolomatskaia & Shulman 2023, Narya docs.

In other dependent type theories

There are other dependent type theories in which it is possible to define indexed semi-simplicial types in a universe:

• A first sketch of a definition was given in by Voevodsky (2012).

• Vladimir Voevodsky proposed Homotopy Type System (HTS), a homotopy type theory extended with non-fibrant types and with an extra equality which is extensional in the sense of extensional type theory;

• Part & Luo (2015) proposed a “Logic-enriched Homotopy Type Theory”, in particular, they formalized a construction of semi-simplicial types in this logic using the Plastic proof assistant;

• Altenkirch, Capriotti & Kraus (2016) proposed a two-level type theory generalizing HTT, leading to 2LTT by Dannil Annenkov?, Paolo Capriotti, Nicolai Kraus and Christian Sattler, providing another construction of semi-simplicial types in an extended type theory;

• According to Kraus (2018), semi-simplicial types can also be constructed in Angiuli-Harper-Wilson’s computational higher-dimensional type theory.

Related concepts

• semi-simplicial object

  • semi-simplicial set

  • semi-simplicial type

• open problems in homotopy type theory

References

Discussion of formulation of semi-simplicial types in the context of homotopy type theory (for use as discussed at category object in an (infinity,1)-category) is in

• UF-IAS-2012, Semi-simplicial types

Coq-code for semi-simplicial types in homotopy type theory had been proposed in

• Vladimir Voevodsky, sketch of a definition (2012) [Coq code]

but its execution requires augmenting homotopy type theory with an auxilirary extensional identity type, discussed in

• Vladimir Voevodsky, A type system with two kinds of identity types (Feb. 2013) [pdf]

See at Homotopy Type System (“HTS”) for more on this.

• Bruno Barras, Thierry Coquand, Simon Huber, A generalization of Takeuti-Gandy Interpretation [pdf]

• Fedor Part?, Zhaohui Luo: Semi-simplicial Types in Logic-enriched Homotopy Type Theory [arXiv:1506.04998] (Submitted on 16 Jun 2015) [Plastic code]

• Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus: Extending Homotopy Type Theory with Strict Equality [arXiv:1604.03799] (Submitted on Apr 2016) [Agda code simulating semi-simplicial types in HoTT with strict equality]

• Danil Annenkov, Paolo Capriotti, Nicolai Kraus, Christian Sattler: Two-Level Type Theory and Applications [arXiv:1705.03307] (Submitted on May 2017)

• Nicolai Kraus, Christian Sattler: Space-valued diagrams, type-theoretically (extended abstract) [arXiv:1704.04543] (Submitted on Apr 2017)

• Nicolai Kraus: On the Role of Semisimplicial Types, 2018 [pdf]

• Astra Kolomatskaia, Semi-Simplicial Types, Homotopy Type Theory Electronic Seminar Talks, 15 December 2022 (slides, video)

• Astra Kolomatskaia, Michael Shulman, Displayed Type Theory and Semi-Simplicial Types [arXiv:2311.18781]

Semi-simplicial types in Narya

• Higher datatypes and codatatypes, Narya documentation. (web)