Powiązanie uniwalencji teorii teorii kości z koncepcją szkieletu

Powiedzmy, że pracuję w teorii typów homotopii, a moim jedynym przedmiotem badań są kategorie konwencjonalne.

Równoważności są podane przez funktory i które zapewniają równoważność kategorii . Istnieją naturalne izomorfizmy i więc ten funktor i „odwrotny” funktor są przekształcane w funktor jednostkowy.$F:{\bf D}\longrightarrow{\bf C}$$G:{\bf C}\longrightarrow{\bf D}$ ${\bf C} \simeq {\bf D}$$\alpha:\mathrm{nat}(FG,1_{\bf C})$$\beta:\mathrm{nat}(GF,1_{\bf D})$

Teraz univalence wiąże równoważność z typem tożsamości teorii typu celowego, którą wybrałem, aby mówić o kategoriach. Ponieważ mam do czynienia tylko z kategoriami, które są równoważne, jeśli mają szkielety izomorficzne , zastanawiam się, czy mogę wyrazić aksjomat jedności w kategoriach przejścia do szkieletu kategorii.${\bf C}={\bf D}$

Albo, inaczej, czy mogę zdefiniować typ tożsamości, tj. Wyrażenie składniowe w sposób, który zasadniczo mówi „istnieje szkielet (lub izomorfi) i i są równoważne. "?${\bf C}={\bf D}:=\dots$${\bf C}$${\bf D}$

(Powyżej staram się interpretować teorię typów w kategoriach pojęć, które są łatwiejsze do zdefiniowania - pojęcia kategorii teoretycznej. Myślę o tym, ponieważ moralnie wydaje mi się, że aksjomat „koryguje” umyślną teorię typów za pomocą twardego kodowania zasada równoważności , który już jest naturalną częścią formułowania wypowiedzi kategorii teoretycznych, np określające obiekty tylko pod względem właściwości uniwersalne).

Odsyłam cię do rozdziału 9 książki HoTT. W szczególności kategoria jest zdefiniowana w taki sposób, aby obiekty izomorficzne były równe, patrz definicja 9.1.6 . Jak wskazuje przykład 9.1.15, w HoTT naprawdę nie ma rozsądnego pojęcia „szkieletowości”. Dzieje się tak, ponieważ równość jest tak słaba, że ​​już oznacza „izomorficzny”.

Co więcej, twierdzenie 9.4.16 mówi

Twierdzenie 9.4.16: Jeśli i są kategoriami, to funkcja (zdefiniowana przez indukcję na funktorze tożsamości) jest równoważnością typów.$A$$B$

$$(A = B) \to (A \simeq B)$$

Twierdzenie mówi nam, że aksjomat Univalence daje nam rodzaj marzenia teoretyka kategorii: równoważne kategorie są równe.

Pytasz, czy możesz zredukować aksjomat Univalence do stwierdzenia o kategoriach. Próby użycia szkieletów nie zadziałają, ponieważ nie ma dobrego sposobu na powiedzenie „szkielet”. Możemy zapytać, czy Twierdzenie 9.4.16 implikuje aksjomat Univalence. O ile mi wiadomo, tak się nie stanie , ponieważ kategoria ma typ (groupoid) obiektów i typ (zestaw) morfizmów, więc twierdzenie 9.4.16 jest równe Aksjomat jednoznaczności tylko dla typów 1.$1$$0$