Relier l'univalence d'une théorie des catéogries au concept de squelette

Disons que je travaille dans la théorie des types d'homotopie et que mes seuls objets d'étude sont des catégories conventionnelles.

Equivalences ici sont donnés par foncteurs et G : C ⟶ D qui fournissent des équivalences de catégories C ≃ D . Il existe des isomorphismes naturels α : n a t ( F G , 1 C ) et β : n a t ( G F , 1 D ) de sorte que ce foncteur et le foncteur "inverse" sont transformés en foncteur unitaire.$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})$

Or, l' univalence relie les équivalences au type d'identité de la théorie du type intentionnel que j'ai choisi de parler des catégories. Puisque je ne traite que des catégories et celles-ci sont équivalentes si elles ont des squelettes isomorphes , je me demande si je peux exprimer l'axiome d'univalence en termes de passage au squelette des catégories.${\bf C}={\bf D}$

Ou, sinon, puis-je définir le type d'identité, c'est-à-dire l'expression syntaxique d'une manière qui dit essentiellement "qu'il y a un squelette (ou des isomorphes) et C et D sont tous deux équivalents".${\bf C}={\bf D}:=\dots$${\bf C}$${\bf D}$

(Dans ce qui précède, j'essaie d'interpréter la théorie des types en termes de concepts plus faciles à définir - les notions théoriques de catégorie. J'y pense parce que moralement, il me semble que l'axiome "corrige" la théorie des types intentionnels en codant en dur le principe d'équivalence , qui fait déjà naturellement partie de la formulation des énoncés théoriques de catégorie, par exemple en ne spécifiant les objets qu'en termes de propriétés universelles.)

Je vous renvoie au chapitre 9 du livre HoTT. En particulier, une catégorie est définie de telle manière que les objets isomorphes sont égaux, voir Définition 9.1.6 . Comme le montre l' exemple 9.1.15 , il n'y a vraiment pas de notion raisonnable de "squelette" dans HoTT. Il en est ainsi parce que l'égalité est si faible qu'elle signifie déjà "isomorphe".

De plus, le théorème 9.4.16 dit

$A$$B$

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

Le théorème nous dit que l'axiome d'univalence nous donne une sorte de rêve de théoricien de catégorie: les catégories équivalentes sont égales.

$1$$0$