Die Univalenz einer Kateogrie-Theorie mit dem Skelett-Konzept in Beziehung setzen

Angenommen, ich arbeite in der Homotopietypentheorie und meine einzigen Studienobjekte sind konventionelle Kategorien.

Äquivalenzen werden hier durch die Funktoren und , die Äquivalenzen der Kategorien liefern . Es gibt natürliche Isomorphismen und so dass dieser Funktor und "inverse" Funktor werden in Einheitsfunktor umgewandelt.$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})$

Die Univalenz bezieht sich nun auf den Identitätstyp der absichtlichen Typentheorie, die ich gewählt habe, um über Kategorien zu sprechen. Da ich mich nur mit Kategorien befasse und diese gleichwertig sind, wenn sie isomorphe Skelette haben , frage ich mich, ob ich das Univalenzaxiom in Bezug auf die Übergabe an das Skelett der Kategorien ausdrücken kann.${\bf C}={\bf D}$

Oder kann ich andernfalls den Identitätstyp definieren, dh den syntaktischen Ausdruck auf eine Weise, die im Wesentlichen sagt: "Es gibt ein Skelett (oder Isomorphi) und und sind beide gleichbedeutend damit. "?${\bf C}={\bf D}:=\dots$${\bf C}$${\bf D}$

(Oben versuche ich, die Typentheorie in Form von Konzepten zu interpretieren, die leichter zu definieren sind - den kategorietheoretischen Begriffen. Ich denke darüber nach, weil es mir moralisch so erscheint, als würde das Axiom die absichtliche Typentheorie durch Hardcodierung "korrigieren" das Äquivalenzprinzip , das bereits ein natürlicher Bestandteil der Formulierung kategorietheoretischer Aussagen ist, z. B. die Angabe von Objekten nur in Bezug auf universelle Eigenschaften.)

Ich verweise Sie auf Kapitel 9 des HoTT-Buches. Insbesondere wird eine Kategorie so definiert, dass isomorphe Objekte gleich sind, siehe Definition 9.1.6 . Wie Beispiel 9.1.15 zeigt, gibt es in HoTT wirklich keinen vernünftigen Begriff von "Skelett". Dies liegt daran, dass die Gleichheit so schwach ist, dass sie bereits "isomorph" bedeutet.

Des Weiteren Satz 9.4.16 sagt

Satz 9.4.16: Wenn und Kategorien sind, ist die Funktion (definiert durch Induktion auf dem Identitätsfunktor) eine Äquivalenz von Typen.$A$$B$

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

Der Satz sagt uns, dass das Univalenz-Axiom uns eine Art Traum eines Katechetheoretikers gibt: Äquivalente Kategorien sind gleich.

Sie fragen, ob Sie das Univalenzaxiom auf eine Aussage über Kategorien reduzieren können. Versuche, Skelette zu verwenden, funktionieren nicht, da es keine gute Möglichkeit gibt, "Skelett" zu sagen. Wir könnten fragen, ob Satz 9.4.16 das Univalenzaxiom impliziert. Soweit ich sehen kann, wird dies nicht der Fall sein, da eine Kategorie einen Typ (Groupoid) von Objekten und einen Typ (Menge) von Morphismen hat, so dass Satz 9.4.16 so etwas wie das ist Univalenzaxiom nur für 1-Typen.$1$$0$