Tags:bicategories, category theory, coq, enriched categories, homotopy type theory and univalent foundations
Abstract:
Enriched categories have found numerous applications, including effects in programming languages, abstract homotopy theory, and in higher category theory. In this abstract, we discuss an ongoing formalization of enriched categories in univalent foundations. More specifically, we define the notion of univalence for enriched categories, and we prove that the bicategory of univalent enriched category is univalent. This gives us a structure identity principle for enriched categories. The definitions and theorems in this abstract are formalized in the Coq proof assistant using the UniMath library \cite{UniMath}.