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 known as Rezk completion.
We provide another construction of the Rezk completion for categories, with the hope that it can be more easily generalized for other (higher) categorical structures. This new construction uses a concept of anonymous objects for categories, which we defined for a general abstract notion of structures.
