Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
category object in an (∞,1)-category, groupoid object
(directed enhancement of homotopy type theory with types behaving like -categories)
The analogue of a Rezk category or complete Segal space in simplicial type theory.
In simplicial type theory, a Rezk type or complete Segal type is a univalent Segal type
Examples of Rezk types include the interval , the -cubes , and the -simplices inductively defined by
The categorical semantics of a complete Segal type is a complete Segal space object in a locally cartesian closed -category .
Emily Riehl, Michael Shulman, A type theory for synthetic -categories arXiv:1705.07442
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)
Last revised on April 10, 2025 at 03:27:21. See the history of this page for a list of all contributions to it.