Universen in abhängiger Typentheorie

11

Ich lese über die Theorie der abhängigen Typen im Online-Buch Homotopy Type Theory .

In Abschnitt 1.3 des Kapitels Typentheorie wird der Begriff der Hierarchie der Universen eingeführt : U0:U1:U2: , wobei

Jedes Universum Ui ist ein Element des nächsten Universums Ui+1 . Darüber hinaus gehen wir davon aus, dass unsere Universen kumulativ sind, dass , dass alle ist die Elemente der ith Universum sind auch Elemente der (i+1)th Universum.

Wenn ich mir jedoch die Formationsregeln für die verschiedenen Typen in Anhang A anschaue, erscheint auf den ersten Blick, wenn ein Universum als Prämisse über dem Balken erscheint, dasselbe Universum darunter. Zum Beispiel für die Regel zur Bildung von Nebenprodukttypen:

ΓA:UiΓB:UiΓA+B:Ui(+-FORM)

Meine Frage ist also, warum eine Hierarchie notwendig ist. Unter welchen Umständen müssen Sie von einem Universum zu einem höheren in der Hierarchie springen? Es ist mir wirklich nicht klar, wie man bei einer Kombination von Am:Ui zu einem Typ B , der nicht in Ui . Im Detail: Die Formationsregeln in den Abschnitten des Anhangs A.2.4, A.2.5, A.2.6, A.2.7, A.2.8, A.2.9, A.2.10, A.3.2 erwähnen entweder Ui in der Prämisse und Urteil, oder nur im Urteil.

Das Buch weist auch darauf hin, dass es einen formalen Weg gibt, Universen zuzuweisen:

Wenn Zweifel daran bestehen, ob ein Argument korrekt ist, können Sie es überprüfen, indem Sie versuchen, allen darin vorkommenden Universen einheitlich Ebenen zuzuweisen.

Wie werden Ebenen konsistent zugewiesen?

U:UUjUij>i

huynhjl
quelle
1
@huynhjl Die Verwendung von Universen ist nicht erforderlich, um Paradoxien zu vermeiden, zum Beispiel weder die ZF-Mengenlehre noch Quines NF, zwei alternative mathematische Grundlagen verwenden sie. Universen sind ein bequemer Weg, um Paradoxien zu vermeiden (oder so hoffen wir) und gleichzeitig die Fähigkeit zu haben, sehr ausdrucksstarke Typen zu konstruieren.
Martin Berger

Antworten:

14

AUi
AUiUiUi:UiU
Γ:ctxΓUi:Ui+1,
Martin Berger
quelle
12

X:UiijX:UjA:U42AU99

ΓX:UiΓY:UiΓ(XY):Ui
XYΠx:XYΠAU42U99U100A:U100und fahren Sie dann fort, um zu zeigen, dass den Typ U 100 hat .AU99U100

ΓX:UiΓY:UjΓ(XY):Umax(i,j)
ΓX:UiΓY:UjikjkΓ(XY):Uk
Andrej Bauer
quelle