Ein fundamentales Rahmenwerk, das die Typentheorie homotopisch interpretiert: Typen gelten als Räume (oder ∞-Gruppoide), Terme als Punkte und Gleichheiten als Pfade, wodurch logische Typenkonstruktoren mit homotopietheoretischer Semantik verschmelzen.

Prinzip

Die Entsprechung zwischen abhängigen Typen und Faserungen nutzen und Identitätstypen als Pfadräume interpretieren, sodass syntaktische Konstruktionen direkte homotopische oder höherkategoriale Bedeutungen haben.

Demonstration

Ein anschauliches Beispiel ist die Interpretation des Univalenz-Axioms: Äquivalenzen zwischen Typen entsprechen Gleichheiten von Typen, modelliert etwa in simplicialen oder kubischen Modellen, in denen Typengleichheiten Homotopie-Äquivalenzen sind.

Fehlanwendung

HoTT-artiges Denken auf klassische, first-order set-theoretische Konstruktionen anzuwenden, ohne höhere homotopische Identifikationen zu beachten, kann zu kategorialen Fehlanpassungen oder dem Verlust extensioneller Argumente führen, die in der Mengenlehre angenommen werden.

Konsequenz

Korrekt angewendet liefert HoTT eine Sprache, um Homotopietheorie innerhalb einer Typentheorie zu betreiben, ermöglicht synthetische Konstruktionen, maschinenprüfbare Formalisierungen und neue Sichtweisen auf Gleichheit, höhere induktive Typen und Univalenz.

Umkehrung

Das Gegenteil sind klassische Mengenlehre-Fundamente, in denen Gleichheit strikt ist und Typen Mengen ohne inhärente Pfadstruktur sind; dort müssen homotopische Identifikationen extern kodiert werden statt als Gleichheit zu erscheinen.

Abgrenzung

HoTT richtet sich auf intensionale abhängige Typentheorien mit homotopischen Modellen; es schließt rein extensional-mengen-theoretische Ansätze aus, sofern sie nicht erweitert werden, und zielt auf Modelle vom ∞-Gruppoidgetyp (simplicial, kubisch, ∞-Topoi).

Semantische Spannung

Spannung besteht zwischen rechnerischen, beweistheoretischen Anforderungen an Typen (Entscheidbarkeit, Normalisierung) und homotopischer Fülle (höhere Identifikationen, Univalenz), was Kompromisse in Sprache und Modellwahl erfordert.

Synthese

HoTT internalisiert homotopietheoretische Ideen in die Typensyntax, sodass Beweise zu homotopischen Konstruktionen werden und ein einheitlicher Formalismus für höherdimensionale Gleichheit, synthetische Topologie und maschinenverifizierbare Mathematik entsteht.