Univalent Enriched Categories and the Enriched Rezk Completion

Technische Samenvatting: Univalente Verrijkte Categorieën en de Rezk-voltooiing

Probleemstelling
Categorietheorie is een fundamenteel kader voor de wiskunde en de informatica, waarbij verrijkte categorieën een cruciale rol spelen in de hogere categorietheorie, homotopietheorie en de semantiek van programmeertalen (bijv. het gebruik van DCPO's voor effectvolle talen). Echter, binnen de context van Univalente Fundamenten (Homotopische Type Theorie), voldoet de standaarddefinitie van categorieën vaak niet aan het principe van equivalentie, dat stelt dat isomorfe objecten ononderscheidbaar zouden moeten zijn. Hoewel "univalente categorieën" (waarbij identiteit van objecten equivalent is aan isomorfisme) al zijn vastgesteld voor gewone categorieën, blijft de theorie van univalente verrijkte categorieën onderontwikkeld. Specifiek is er een gebrek aan geformaliseerde resultaten met betrekking tot het structuuridentiteitsprincipe, de karakterisering van equivalenties en het bestaan van een Rezk-voltooiing (een univalente reflectie) voor verrijkte categorieën. Bovendien zijn standaardconstructies zoals Kleisli-categorieën vaak niet univalent, wat een methode vereist om univalente analogen binnen de verrijkte setting te construeren.

Methodologie
Het artikel ontwikkelt de theorie van verrijkte categorieën binnen de Rocq-bewijsassistent met behulp van de UniMath-bibliotheek, waarbij wordt aangesloten bij de Univalente Fundamenten. De kern van de methodologische aanpak omvat:

1. Verrijkingen als Structuur: In plaats van verrijkte categorieën te definiëren als een verzameling objecten en hom-objecten (de Kelly-definitie), definiëren de auteurs deze als een categorie samen met een verrijking. Een verrijking bestaat uit hom-objecten in een monoidale categorie $\mathcal{V}$, identiteit en compositie-morfismen, en een correspondentie tussen morfismen in de onderliggende categorie en elementen van de hom-objecten. Dit perspectief behandelt een verrijkte categorie als een univalente categorie met extra structuur.
2. Gedisplayde Bicategorieën: Om het structuuridentiteitsprincipe te bewijzen, maken de auteurs gebruik van de machinerie van gedisplayde bicategorieën. Ze definiëren een gedisplayde bicategorie $dEnrichCat_{\mathcal{V}}$ over de bicategorie van univalente categorieën ($UnivCat$). De totale bicategorie van deze display is $EnrichCat_{\mathcal{V}}$. Dit maakt het mogelijk om bestaande univalentie-resultaten voor $UnivCat$ te hergebruiken om univalentie voor de verrijkte setting te bewijzen.
3. Orthogonale Factorisatiesystemen: Om equivalenties te karakteriseren, gebruikt het artikel orthogonale factorisatiesystemen in bicategorieën. Het definieert volledig begrensde (fully faithful) en essentieel surjectieve verrijkte functoren en bewijst dat deze een orthogonaal factorisatiesysteem vormen.
4. Twee Constructies van de Rezk-voltooiing: Het artikel biedt twee verschillende constructies voor de Rezk-voltooiing van een verrijkte categorie:
   • Yoneda-inbedding: Het construeren van de voltooiing als de afbeelding van de verrijkte Yoneda-inbedding. Dit vereist dat $\mathcal{V}$ volledig en symmetrisch monoidaal gesloten is, maar steunt op de standaard categorietheorie.
   • Hogere Inductieve Typen (HITs): Het construeren van de voltooiing door de Rezk-voltooiing van de onderliggende categorie te voorzien van een verrijking met behulp van de eliminatieregels van HIT's. Deze aanpak vermijdt aannames over volledigheid of geslotenheid van $\mathcal{V}$ en behoudt universe-niveaus als het universum gesloten is onder HIT's.
5. Universele Eigenschappen: Het artikel vestigt de universele eigenschap van de Rezk-voltooiing, door aan te tonen dat precompositie met een zwakke equivalentie (volledig begrensde en essentieel surjectieve functor) een adjunct equivalentie induceert tussen functor-categorieën.

Belangrijkste Bijdragen en Resultaten

• Structuuridentiteitsprincipe: Het artikel bewijst dat de bicategorie van univalente verrijkte categorieën ($EnrichCat_{\mathcal{V}}$) univalent is (Stelling 2.8). Dit impliceert dat het identiteitstype tussen twee univalente verrijkte categorieën equivalent is aan de type van adjuncte equivalenties tussen hen.
• Karakterisering van Equivalenties: Er wordt bewezen dat elke verrijkte functor die zowel volledig begrensd als essentieel surjectief is, een adjuncte equivalentie is (Stelling 4.8). Dit resultaat is constructief en steunt op het feit dat het domein en codomein univalent zijn, waardoor de keuzeaxioma wordt vermeden.
• Rezk-voltooiing: Twee constructies voor de Rezk-voltooiing van verrijkte categorieën worden geboden (Constructies 5.5 en 5.7). Het artikel bewijst dat elke verrijkte categorie een Rezk-voltooiing bezit en voldoet aan de universele eigenschap dat elke functor naar een univalente verrijkte categorie zich uniek voortzet langs zwakke equivalenties (Stelling 5.2).
• Univalente Kleisli-categorieën: De auteurs construeren univalente verrijkte Kleisli-categorieën. Ze definiëren de standaard Kleisli-categorie $K(T)$ en de univalente tegenhanger $Kleisli(T)$ (als een volledige subcategorie van de Eilenberg-Moore categorie). Met behulp van de Rezk-voltootiing en de universele eigenschap laten ze zien dat $Kleisli(T)$ de universele eigenschap van Kleisli-objecten in de bicategorie van univalente verrijkte categorieën vervult (Constructie 6.9).
• Voorbeelden en Karakteriseringen: Het artikel biedt talrijke voorbeelden, waaronder zelf-verrijking, opposite verrijkingen en veranderingen van basis. Het karakteriseert verrijkingen over Cartesiaanse structuren (zoals DCPO's) en introduceert een begrip van "gesloten structuur die smash-producten ondersteunt" om gepunteerde verzamelingen en posets te behandelen, hoewel het beperkingen opmerkt met betrekking tot gepunteerde DCPO's.

Betekenis en Claims
Het artikel claimt een robuuste fundering voor de verrijkte categorietheorie binnen de Univalente Fundamenten te hebben gelegd. De primaire betekenis ligt in:

1. Formalisering: Het leveren van een geformaliseerde bibliotheek in Rocq/UniMath voor verrijkte categorieën, die voorheen minder uitgebreid geformaliseerd was vergeleken met gewone categorieën.
2. Correctheid van Begrip: Het aantonen dat het beschouwen van verrijkte categorieën als univalente categorieën met extra structuur (via verrijkingen) bewijzen van fundamentele eigenschappen zoals het structuuridentiteitsprincipe vereenvoudigt.
3. Oplossen van Niet-Univalentie: Het aanpakken van het probleem dat veel constructies (zoals Kleisli-categorieën) inherent niet univalent zijn, door een systematische methode (Rezk-voltooiing) te bieden om univalente versies te verkrijgen die de noodzakelijke universele eigenschappen behouden.
4. Fundamentele Instrumenten: Het vestigen van de bicategorie van univalente verrijkte categorieën als een univalente bicategorie, wat een vereiste is voor het ontwikkelen van verdere interne categorietheorie (bijv. monaden, limieten) in een univalente setting.

De auteurs merken op dat hoewel hun aanpak veel standaardgevallen dekt, er beperkingen zijn met betrekking tot smash-producten voor bepaalde structuren (zoals gepunteerde DCPO's) waar quotienten genomen moeten worden in de passende categorie in plaats van in verzamelingen. Ze suggereren dat toekomstig werk het kunnen omvatten van het ontwikkelen van de uitrusting van verrijkte categorieën of het generaliseren van het begrip smash-product om deze gevallen te behandelen.