Towards Rezk Completion for Higher Categorical Structures
When studying categories in homotopy type theory, it turns out that the well-behaved definition is that of univalent categories, that is, categories such that isomorphisms between objects are equivalent to identities between them. It has been shown that any category is weakly equivalent to a univalent one; this operation is…
