Ist die Theorie des kubischen Typs immer noch mit der einwertigen ausgeschlossenen mittleren und einwertigen Wahl vereinbar?

Question

Ich möchte einige Grundkenntnisse in Mathematik im kubischen Agda formalisieren und dabei die Theorie kubischer Typen erlernen.Das Problem ist, dass ich eine einwertige ausgeschlossene mittlere und eine einwertige Auswahl (und möglicherweise eine propositionale Größenänderung) benötige.Ich weiß, dass diese mit der Homotopietypentheorie übereinstimmen (obwohl die Berechnung verloren geht, wenn Axiome verwendet werden), aber kubisch ist diese Typentheorie stärker (in dem Sinne, dass Univalenz ein Theorem ist).Ist dieses Axiom im kubischen Kontext noch konsistent?Gibt es eine bessere Möglichkeit, klassische Theoreme in der Theorie kubischer Typen anzuwenden?

Answer 1

Ich beschloss, meine Antwort neu zu schreiben, weil ich dachte, ich könnte die Details besser erklären.Ich würde mich immer noch jemandem verschieben, der mehr kennt, falls er zufällig mitkommt.

Ich denke, man kann relativ sicher sagen, dass die kubische Typentheorie ein Ansatz ist im Großen und Ganzen ist mit den gewünschten klassischen Axiomen kompatibel.Die Gründe dafür sind:

1. Die Unterschiede Menschen normalerweise darauf hinweisen, wie die $\mathsf{Kleber}$ Typ, sind nur eine Möglichkeit, Univalenz zu halten für alle Typen, unabhängig von ihrer Zugehörigkeit zu einem Universum.Dies ist (meiner Ansicht nach) lediglich eine Einschränkung des HOTT-Ansatzes der minimalen Erweiterung der Martin-Löf-Theorie, wobei es unmöglich ist, das Univalenz-Axiom zu sagen, außer in Bezug auf ein Universum.Wenn Sie jedoch genügend Universen mit Univalenz -Axiomen haben, befindet sich jeder Typ in einem Universum, und so gilt die Univalenz für alle Typen.Tatsächlich funktioniert Agda direkt so;Die Universen sind primär und alle Typen werden als Teil eines Universums deklariert, ähnlich wie ein reines Typsystem.

2. Es gibt (ich habe gehört) ein kubisches Set -Modell (entdeckt von Emily Riehl), das vollständig mit dem Standardmodell Simplicial Set kompatibel ist, und ich glaube, es hat sich als angemessen für die kubische Typtheorie erwiesen.Ich denke, das bedeutet, dass Sie, wenn Sie sie hinzufügen (und vielleicht die Wahl) hinzufügen, dieselbe Homotopie -Theorie wie das klassische Einfach -Set -Modell.Ich habe auch gehört, dass es konstruktive Analoga des Simplicial Set -Modells gibt, daher ist es nicht von Natur aus klassisch.

Nun müssen Sie sich um andere Details kümmern.Zum Beispiel verwendet die kubische AgDA die Art von Würfeln mit Inversionen und Verbindungen.Also, wenn i Und j sind dann Dimensionsvariablen ~ i ist eine Dimension, und das ist sie auch i ∨ j.Es gibt auch kartesische Würfel, die nicht haben ∨ haben aber andere ähnliche Konstruktionen.Diese wirken sich auf die Details aus, wie Sie Pfade konstruieren können.Mehr von ihnen zu haben ist bequem, um leicht Kompositionen von Pfaden und so weiter zu konstruieren, aber ich verstehe, dass das Modell, das dem klassischen simple -Modell entspricht, den meisten dieser Dinge fehlt.

Insbesondere habe ich auch gehört, dass die meisten dieser anderen kubischen Set -Modelle Sind antiklassisch (das hatte ich vorhin vergessen).Ich konnte die Details darüber nicht herausfinden, wie Sie dies demonstrieren innen implementierte kubische Typ -Theorien, aber mein Verständnis ist das, das verwendet wird ~ Als Beispiel versuchen Sie, ein widersprüchliches Szenario mit einem Punkt zu konstruieren i in der Pause so dass i = ~i.Es gibt keine Möglichkeit in der Typtheorie, einen solchen Punkt zu konstruieren, und irgendwie ist es inkonsistent anzunehmen, dass Sie feststellen können, ob ein abstrakter Punkt so ist oder nicht.

Ich vermute also, dass die Antwort auf Ihre spezifische Frage lautet: Ja wahrscheinlich Eine Möglichkeit, die ausgeschlossene Mitte in der kubischen AGDA (obwohl ich nicht weiß, wie) und jeder andere Computer die kubische Typentheorie implementiert.Es ist aber auch wahrscheinlich, dass eine kubische Typtheorie implementiert werden kann, die mit klassischen Axiomen (und Homotopie -Theorie) übereinstimmt und alle gewünschten Argumente unterstützt (obwohl es vielleicht schwieriger ist, bestimmte Dinge zu konstruieren).Leider müssen Sie wahrscheinlich warten, bis die Details genauer ausgearbeitet sind und sich einige Implementierungen dazu entschließen, die kompatible Version der Theorie zu übernehmen.

Eine andere Möglichkeit besteht meiner Meinung nach darin, sich nicht zu viele Gedanken über den antiklassischen Teil zu machen.Wenn Sie die kubischen Grundelemente verwenden, um etwas Ähnliches wie die Argumentation im HoTT-Buch zu implementieren, und es vermeiden, direkt mit den kubischen Operationen zu arbeiten, können Sie (glaube ich) einigermaßen sicher sein, dass Sie sich nicht auf irgendwelche Paradoxien verlassen haben.Ich denke, dass es in einigen der verfügbaren Bibliotheken Bestrebungen gibt, zusätzlich zur kubischen Typtheorie eine HoTT-Schnittstelle bereitzustellen.Sie könnten sich auch daran versuchen, die direkten kubischen Teile zu lernen, auch wenn Sie sie nicht direkt verwenden, obwohl ich nicht genau weiß, welche Teile noch Teil des „richtigen“ Modells sind.

Bearbeiten:Übrigens, Hier ist eine Präsentation über kubische Mengenmodelle der Homotopietypentheorie, die die antiklassischen Eigenschaften vieler kubischer Mengenmodelle erwähnt.Es beschreibt vage, was Sie tun müssen, um die ausgeschlossene Mitte zu widerlegen, aber es geht nur darum, die Modelle von außen zu betrachten, daher ist es (für mich) teilweise schwierig, dies in eine Widerlegung innerhalb der kubischen Typentheorie umzusetzen.

Bearbeiten 2:Hier ist eine möglicherweise positivere Antwort.Ich wurde darauf hingewiesen, dass die Konstruktionen im obigen Video möglicherweise nicht innerhalb der kubischen Typentheorie ausgeführt werden können.Es handelt sich um Konstruktionen, die in den „vorgesehenen“ kubischen Mengenmodellen ausgeführt werden können, aber genau wie die Martin-Löf-Typentheorie andere Modelle als das beabsichtigte hat (so gelangt man zu HoTT), sind die kubischen Mengenmodelle nicht unbedingt notwendig das einzige Modell der entsprechenden kubischen Typentheorie.Daher ist es möglich, dass kubische Typtheorien mit der ausgeschlossenen Mitte und der Wahl kompatibel sind, auch wenn dies bei ihren offensichtlichsten Modellen nicht der Fall ist.