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 framework for lifting the Rezk completion from categories to categories with structure. We demonstrate the modularity of our framework by lifting the Rezk completion from categories to elementary topoi in manageable steps.

翻译：在单值基础中发展范畴论及其形式化是一个活跃的研究领域。该设定下的范畴通常被假定为单值的，这意味着对象的恒等态射与同构态射是重合的。由此产生的一个结果是，对于单值范畴而言，等价性与恒等性是重合的，并且单值范畴上的结构可以沿着等价关系进行传递。然而，诸如Kleisli范畴、Karoubi包络以及tripos-to-topos构造等构建方法，并不必然产生单值范畴。为解决这一问题，研究者采用了Rezk完备化方法，该方法可将一个范畴完备化为单值范畴。然而，当考虑带结构的范畴时，要使用Rezk完备化，还需要证明Rezk完备化能够继承原始范畴的结构。在本工作中，我们提出了一个模块化框架，用于将Rezk完备化从普通范畴提升至带结构的范畴。我们通过将Rezk完备化从范畴逐步提升至初等拓扑斯的可控步骤，展示了该框架的模块化特性。