nLab Rezk complete type (changes)

Showing changes from revision #5 to #6: Added | Removed | Changed

This article is about arbitrary types satisfying the Rezk completion condition in simplicial type theory. For synthetic pre-categories satisfying the Rezk completion condition, see Rezk type

---

\tableofcontents

Definition

In simplicial type theory, let $\mathrm{iso}_A(x, y)$ be some notion of isomorphism.

\begin{definition} A type $A$ is a Rezk complete type if the canonical function which by the J rule takes an identification of elements $p:x =_A y$ to an isomorphism $J(\lambda t.\mathrm{id}_A(t), x, y, p):\mathrm{iso}_A(x, y)$ is an equivalence of types for all $x:A$ and $y:A$.

\end{definition}

Equivalently, let $\mathbb{E}$ denote the free-standing isomorphism, for some notion of isomorphism. For example, the free-standing bi-invertible morphism $\mathbb{E}$ can be defined as a colimit on a diagram involving the simplicial interval $\mathbb{I}$ (see Sterling & Ye 2025). There is a unique function $u_\mathbb{E}:\mathbb{E} \to \mathbb{I}_h$ to the homotopical interval higher inductive type $\mathbb{I}_h$ by the universal property of the negative unit type and the equivalence of $\mathbb{I}_h$ with the negative unit type.

\begin{definition} A type $A$ is a Rezk complete type if the canonical function

is an equivalence of types

\end{definition}

Related concepts

• simplicial type theory
• isomorphism in simplicial type theory
• simplicially discrete type
• Rezk type
• gaunt Segal type
• univalent category

References

• Ulrik Buchholtz, Jonathan Weinberger, Synthetic fibered $(\infty,1)$-category theory $[$arXiv:2105.01724, talk slides$]$

• Jonathan Sterling, Lingyuan Ye, Domains and Classifying Topoi (arXiv:2505.13096)