nLab Segal type

 Idea

The analogue of a Segal space in simplicial type theory. A Segal type is a type $A$ such that every pair of composable morphisms to $z:A$ is uniquely composable.

Definition

Using morphisms

Definition

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(y, z)$, the type

$$\sum_{h:\mathrm{hom}_A(x, z)} \sum_{k:\Delta^2 \to A} \left( \begin{array}{c} (k(0, 0) = x) \times (k(0, 1) = y) \times (k(1, 1) = z) \times \\ (k_{(0, 0), (0, 1)} = f) \times (k_{(0, 1), (1, 1)} = g) \times (k_{(0, 0), (1, 1)} = h) \end{array} \right)$$

is a contractible type, where $\Delta^2 \coloneqq \sum_{(s, t):\mathbb{I} \times \mathbb{I}} s \leq t$ is the 2-simplex type.

Definition

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)$,

$$\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.

Using functions from shapes

In simplicial type theory where the directed interval primitive $\mathbb{I}$ is defined via axioms, let the 2-simplex type be defined as

$$\Delta^2 \coloneqq \sum_{s:\mathbb{I}} \sum_{t:\mathbb{I}} s \leq t$$

and let the (2,1)-horn type be defined as

$$\Lambda_1^2 \coloneqq \sum_{s:\mathbb{2}} \sum_{t:\mathbb{2}} (s =_\mathbb{I} 0) \vee (t =_\mathbb{I} 1)$$

where $P \vee Q$ is the disjunction of the types $P$ and $Q$. Since $s \leq t$ implies $(s =_{\mathbb{I}} 0) \vee (t =_{\mathbb{I}} 1)$ for all $s:\mathbb{I}$ and $t:\mathbb{I}$, we have a canonical function

$$(\lambda t:\mathbb{I}.t, \lambda t:\mathbb{I}.t, P):\Delta^2 \to \Lambda^2_1$$

which is a tuple consisting of two copies of the identity function on $\mathbb{I}$ and a dependent function $P$ that takes the witness that $s \leq t$ to a witness that $(s =_{\mathbb{I}} 0) \vee (t =_{\mathbb{I}} 1)$. By precomposition, this leads to a function

$$\lambda u.u \circ (\lambda t:\mathbb{I}.t, \lambda t:\mathbb{I}.t, P):(\Delta^2 \to A) \to (\Lambda^2_1 \to A)$$

for all types $A$.

Definition

$A$ is a Segal type if the above function is an equivalence of types.

$$\mathrm{isSegal}(A) \coloneqq \mathrm{isEquiv}(\lambda u.u \circ (\lambda t:\mathbb{I}.t, \lambda t:\mathbb{I}.t, P))$$

 Categorical semantics

The categorical semantics of a Segal type is a Segal space object in a locally cartesian closed $(\infty,1)$-category $\mathbf{H}$.

Related concepts

• hom type
• discrete Segal type
• Rezk type
• isomorphism in a Segal type
• Segal space
• precategory
• skeletal Segal type

References

• 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)