nLab Rezk type

Idea

The analogue of a Rezk category or complete Segal space in simplicial type theory.

Definition

In simplicial type theory, a Rezk type or complete Segal type is a univalent Segal type

$$\mathrm{isRezk}(A) \coloneqq \mathrm{isSegal}(A) \times \mathrm{isUnivalent}(A)$$

 Examples

Examples of Rezk types include the interval $\mathbb{I}$, the $n$-cubes $\mathrm{Fin}(n) \to \mathbb{I}$, and the $n$-simplices inductively defined by

$$\Delta^0 \coloneqq \mathrm{Fin}(0) \to \mathbb{I}$$

$$n:\mathbb{N} \vdash \Delta^{n + 1} \coloneqq \sum_{t:\mathrm{Fin}(n + 1) \to \mathbb{I}} \prod_{i:\mathrm{Fin}(n)} t(\pi_1(i)) \leq t(\pi_1(i + 1))$$

 Categorical semantics

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

Related concepts

• Segal type
• univalent type
• simplicially discrete type
• complete Segal space
• univalent category
• skeletal Segal type
• gaunt 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)