The Rezk Completion for Elementary Topoi
Kobe Wullaert, Niels van der Weide

TL;DR
This paper develops a modular framework to extend the Rezk completion process from basic categories to structured categories like elementary topoi within univalent foundations, ensuring structure inheritance.
Contribution
It introduces a modular approach for lifting the Rezk completion to categories with structure, demonstrated on elementary topoi.
Findings
Framework successfully lifts Rezk completion to elementary topoi.
Ensures structure inheritance during the Rezk completion process.
Facilitates formalization of structured categories in univalent foundations.
Abstract
The development of category theory in univalent foundations and the formalization thereof is an active field of research. Categories in that setting are often assumed to be univalent which means that identities and isomorphisms of objects coincide. One consequence hereof is that equivalences and identities coincide for univalent categories and that structure on univalent categories transfers along equivalences. However, constructions such as the Kleisli category, the Karoubi envelope, and the tripos-to-topos construction, do not necessarily give univalent categories. To deal with that problem, one uses the Rezk completion, which completes a category into a univalent one. However, to use the Rezk completion when considering categories with structure, one also needs to show that the Rezk completion inherits the structure from the original category. In this work, we present a modular…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHomotopy and Cohomology in Algebraic Topology · Logic, programming, and type systems · Model-Driven Software Engineering Techniques
