Univalent Enriched Categories and the Enriched Rezk Completion
Abstract
Enriched categories are categories whose sets of morphisms are enriched with extra structure. Such categories play a prominent role in the study of higher categories, homotopy theory, and the semantics of programming languages. In this paper, we study univalent enriched categories. We prove that all essentially surjective and fully faithful functors between univalent enriched categories are equivalences, and we show that every enriched category admits a Rezk completion. Finally, we use the Rezk completion for enriched categories to construct univalent enriched Kleisli categories.
Fields of Study & Subjects
Homotopy and Cohomology in Algebraic Topology
Algebraic structures and combinatorial models
Publication details
- Journal / source
- Logical Methods in Computer Science
- Publisher
- Centre pour la Communication Scientifique Directe (CCSD)
- Volume
- Volume 22, Issue 2
- Publication date
- 2 June 2026
- Language
- EN