(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
There are multiple different formalisms of simplicial homotopy type theory; two of them are given in Gratzer, Weinberger, & Buchholtz 2024 and in Riehl & Shulman 2017, and in each formalism there is a different way to define Segal types.
In simplicial homotopy type theory where the directed interval primitive $\mathbb{2}$ is defined via axioms, let the 2-simplex type be defined as
and let the 2-1-horn type be defined as
where $[P]$ is the propositional truncation of the type $P$. For each type $A$ there is a canonical restriction function $i:(\Delta^2 \to A) \to (\Lambda_1^2 \to A)$.
$A$ is a Segal type if the restriction function $i$ is an equivalence of types.
In simplicial type theory in the type theory with shapes formalism, 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(y, z)$, the type
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$]$
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)
Last revised on October 5, 2024 at 17:53:17. See the history of this page for a list of all contributions to it.