nLab Rezk type

Context

(,1)(\infty,1)-Category theory

Internal (,1)(\infty,1)-Categories

Directed homotopy type theory

Contents

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

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

 Examples

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

Δ 0Fin(0)𝕀\Delta^0 \coloneqq \mathrm{Fin}(0) \to \mathbb{I}
n:Δ n+1 t:Fin(n+1)𝕀 i:Fin(n)t(π 1(i))t(π 1(i+1))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 ( , 1 ) (\infty,1) -category H\mathbf{H}.

References

Last revised on April 10, 2025 at 03:27:21. See the history of this page for a list of all contributions to it.