(directed enhancement of homotopy type theory with types behaving like $(\infty,n)$-categories)

Segal types are the (infinity,1)-categorical version of precategories in simplicial type theory

In simplicial type theory, a **Segal type** is a type $A$ such that given elements $x:A$, $y:A$, and $z:A$ and morphisms $f:\mathrm{hom}_A(x, y)$ and $g:\mathrm{hom}_A(x, y)$, the type

$\sum_{h:\mathrm{hom}_A(x, z)} \left\langle \Delta^2 \to A \vert_{[x, y, z, f, g, h]}^{\partial \Delta^2} \right\rangle$

is a contractible type, where $\Delta^2$ is the $2$-simplex probe shape and $\partial \Delta^2$ is its boundary.

- Emily Riehl, Michael Shulman,
*A type theory for synthetic $\infty$-categories*$[$arXiv:1705.07442$]$

Last revised on September 19, 2023 at 14:36:52. See the history of this page for a list of all contributions to it.