Gibt es eine Korrespondenz zwischen dem Summentyp in der Typentheorie und der arithmetischen Summation?

Question

Gibt es eine Korrespondenz zwischen dem Coproduct (SUM) Typ in der Typentheorie und der arithmetischen Summation?

Zum Beispiel, was bedeutet 3 + 4 oder x + 6 in der Typentheorie?

Answer 1

Die arithmetische Notation in der Typentheorie ist mit dem Verhalten auf Sätzen motiviert, in dem die disjunkte Union $ A + B $ $ | A | + | B | $ Elemente; Das kartesische Produkt hat $ | A | \ mal | b | $ Elemente; Und der Satz von Funktionen $ B ^ A $ hat $ | B | ^ {| a |} $ Elemente. Summe, Produkt- und Funktionstypen erfüllen viele der üblichen Identitäten, die Sie von Arithmetik erwarten (wenn auch typischerweise bis zum Isomorphismus, anstatt der Gleichheit).

das Papier Objekte von Kategorien als komplexe Zahlen von Marcelo Fiore und Tom Leinster erforscht dies in Einige Details, obwohl es hilft, ein wenig Erfahrung mit Algebra- oder Kategorie-Theorie zu haben.

Manchmal wird eine natürliche Zahl $ n $ einen Typ mit genau $ n $ Begriffe in jedem bezeichnen Kontext (analog zu einem Set mit $ n $ Elemente). In dieser Einstellung $ 3 + 4 \ CONG 7 $ als Typen. $ x + 6 $ ist nicht gut geformt, ohne $ x $ in einem bestimmten Kontext zu platzieren.