Niels van der Weide - Univalent Enriched Categories and the Enriched Rezk Completion

lmcs:15947 - Logical Methods in Computer Science, June 2, 2026, Volume 22, Issue 2 - https://doi.org/10.46298/lmcs-22(2:25)2026
Univalent Enriched Categories and the Enriched Rezk CompletionArticle

Authors: Niels van der Weide

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.


Volume: Volume 22, Issue 2
Secondary volumes: Selected Papers of the 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Published on: June 2, 2026
Accepted on: April 17, 2026
Submitted on: June 27, 2025
Keywords: Logic in Computer Science, Category Theory

Consultation statistics

This page has been seen 20 times.
This article's PDF has been downloaded 3 times.