Univalent Enriched Categories and the Enriched Rezk Completion

Technical Summary: Univalent Enriched Categories and the Enriched Rezk Completion

Problem Statement
Category theory is a foundational framework for mathematics and computer science, with enriched categories playing a critical role in higher category theory, homotopy theory, and the semantics of programming languages (e.g., using DCPOs for effectful languages). However, within the context of Univalent Foundations (Homotopy Type Theory), the standard definition of categories often fails to satisfy the principle of equivalence, which states that isomorphic objects should be indistinguishable. While "univalent categories" (where identity of objects is equivalent to isomorphism) have been established for ordinary categories, the theory of univalent enriched categories remains underdeveloped. Specifically, there is a lack of formalized results regarding the structure identity principle, the characterization of equivalences, and the existence of a Rezk completion (a univalent reflection) for enriched categories. Furthermore, standard constructions like Kleisli categories often fail to be univalent, necessitating a method to construct univalent analogues within the enriched setting.

Methodology
The paper develops the theory of enriched categories within the Rocq proof assistant using the UniMath library, adhering to Univalent Foundations. The core methodological approach involves:

1. Enrichments as Structure: Instead of defining enriched categories as a collection of objects and hom-objects (the Kelly definition), the authors define them as a category together with an enrichment. An enrichment consists of hom-objects in a monoidal category $\mathcal{V}$, identity and composition morphisms, and a correspondence between morphisms in the underlying category and elements of the hom-objects. This perspective treats an enriched category as a univalent category equipped with extra structure.
2. Displayed Bicategories: To prove the structure identity principle, the authors utilize the machinery of displayed bicategories. They define a displayed bicategory $dEnrichCat_{\mathcal{V}}$ over the bicategory of univalent categories ($UnivCat$). The total bicategory of this display is $EnrichCat_{\mathcal{V}}$. This allows the reuse of existing univalence results for $UnivCat$ to prove univalence for the enriched setting.
3. Orthogonal Factorization Systems: To characterize equivalences, the paper employs orthogonal factorization systems in bicategories. It defines fully faithful and essentially surjective enriched functors and proves they form an orthogonal factorization system.
4. Two Constructions of Rezk Completion: The paper provides two distinct constructions for the Rezk completion of an enriched category:
   • Yoneda Embedding: Constructing the completion as the image of the enriched Yoneda embedding. This requires $\mathcal{V}$ to be complete and symmetric monoidal closed but relies on standard category theory.
   • Higher Inductive Types (HITs): Constructing the completion by endowing the Rezk completion of the underlying category with an enrichment using the elimination rules of HITs. This approach avoids assumptions of completeness or closedness in $\mathcal{V}$ and preserves universe levels if the universe is closed under HITs.
5. Universal Properties: The paper establishes the universal property of the Rezk completion, demonstrating that precomposition with a weak equivalence (fully faithful and essentially surjective functor) induces an adjoint equivalence between functor categories.

Key Contributions and Results

• Structure Identity Principle: The paper proves that the bicategory of univalent enriched categories ($EnrichCat_{\mathcal{V}}$) is univalent (Theorem 2.8). This implies that the identity type between two univalent enriched categories is equivalent to the type of adjoint equivalences between them.
• Characterization of Equivalences: It is proven that every enriched functor that is both fully faithful and essentially surjective is an adjoint equivalence (Theorem 4.8). This result is constructive and relies on the domain and codomain being univalent, avoiding the axiom of choice.
• Rezk Completion: Two constructions for the Rezk completion of enriched categories are provided (Constructions 5.5 and 5.7). The paper proves that every enriched category admits a Rezk completion and satisfies the universal property that any functor to a univalent enriched category extends uniquely along weak equivalences (Theorem 5.2).
• Univalent Kleisli Categories: The authors construct univalent enriched Kleisli categories. They define the standard Kleisli category $K(T)$ and its univalent counterpart $Kleisli(T)$ (as a full subcategory of the Eilenberg-Moore category). Using the Rezk completion and the universal property, they show that $Kleisli(T)$ satisfies the universal property of Kleisli objects in the bicategory of univalent enriched categories (Construction 6.9).
• Examples and Characterizations: The paper provides numerous examples, including self-enrichment, opposite enrichments, and changes of base. It characterizes enrichments over Cartesian structures (like DCPOs) and introduces a notion of "closed structure supporting smash products" to handle pointed sets and posets, though it notes limitations regarding pointed DCPOs.

Significance and Claims
The paper claims to establish a robust foundation for enriched category theory within Univalent Foundations. Its primary significance lies in:

1. Formalization: Providing a formalized library in Rocq/UniMath for enriched categories, which previously lacked extensive formalization compared to ordinary categories.
2. Correctness of Notion: Demonstrating that viewing enriched categories as univalent categories with extra structure (via enrichments) simplifies proofs of fundamental properties like the structure identity principle.
3. Resolution of Non-Univalence: Addressing the issue that common constructions (like Kleisli categories) are not inherently univalent by providing a systematic method (Rezk completion) to obtain univalent versions that preserve the necessary universal properties.
4. Foundational Tools: Establishing the bicategory of univalent enriched categories as a univalent bicategory, which is a prerequisite for developing further internal category theory (e.g., monads, limits) in a univalent setting.

The authors note that while their approach covers many standard cases, it has limitations regarding smash products for certain structures (like pointed DCPOs) where quotients must be taken in the appropriate category rather than sets. They suggest future work could involve developing the equipment of enriched categories or generalizing the smash product notion to handle these cases.