nLab Rezk complete type

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

---

Definition

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

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

$$\mathrm{isRezkComplete}(A) \coloneqq \prod_{x:A} \prod_{y:A} \mathrm{isEquiv}(\lambda p.J(\lambda t.\mathrm{id}_A(t), x, y, p))$$

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.

Definition

A type $A$ is a Rezk complete type if the canonical function

$$\lambda f.f \circ u_\mathbb{E}:(\mathbb{I}_h \to A) \to (\mathbb{E} \to A)$$

is an equivalence of types

$$\mathrm{isRezkComplete}(A) \coloneqq \mathrm{isEquiv}(\lambda f.f \circ u_\mathbb{E})$$

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)