Was sind die Gleichungsgesetze für Nulltypen?

Haftungsausschluss : Während ich mich für Typentheorie interessiere, betrachte ich mich selbst nicht als Experten für Typentheorie.

Im einfach getippten Lambda-Kalkül hat der Null-Typ keine Konstruktoren und einen eindeutigen Eliminator:

$$\frac{\Gamma \vdash M \colon 0}{\Gamma \vdash initial (M) \colon A}$$

Aus denotational Sicht der Gleichung $initial (M_1) = initial(M_2)$ ist offensichtlich , (wenn die Typen sinnvoll).

Aus dieser Perspektive kann ich jedoch auch ableiten, dass, wenn $M,M' \colon 0$ , dann: $M = M'$ . Dieser Abzug scheint stärker zu sein, obwohl mir ein bestimmtes Modell, das dies zeigt, entgeht.

(Ich habe allerdings einige Beweistheoretische Anschauungen: Es spielt keine Rolle, welchen Widerspruch Sie verwenden, um einen Einwohner zu erhalten, aber es kann verschiedene Widerspruchsbeweise geben.)

Meine Fragen sind also:

1. Was sind die Standardgleichungsgesetze für Nulltypen?
2. Sind einige von ihnen als $\eta$ oder $\beta$ Gesetze klassifiziert ?

1. Die Standardgleichungsregeln für den leeren Typ lauten , wie Sie vermuten, . Denken Sie an das standardmäßige satztheoretische Modell, bei dem Mengen nach Typen interpretiert werden: Summentypen sind disjunkte Vereinigungen, und der leere Typ ist die leere Menge. Also müssen auch zwei beliebige Funktionen e , e ' : Γ → 0 gleich sein, da sie einen gemeinsamen Graphen haben (nämlich den leeren Graphen). .$\Gamma \vdash e = e' : 0$$e,e' : \Gamma \to 0$

2. Der leere Typ hat keine Regeln, da es keine Einführungsformulare dafür gibt. Seine einzige Gleichungsregel ist ein $\beta$$\eta$ Regel. Abhängig davon, wie streng Sie interpretieren möchten, was eine eta-Regel ist, möchten Sie diese möglicherweise in ein plus eine Pendelumwandlung aufteilen. Die strenge η- Regel lautet:$\eta$$\eta$

   $$e = \mathrm{initial}(e)$$

   Die Pendlerversicherung lautet:

   $$C[\mathrm{initial}(e)] = \mathrm{initial}(e)$$

BEARBEITEN:

Deshalb impliziert die Verteilung beim Null-Typ die Gleichheit aller Abbildungen .$A \to 0$

Um die Notation zu korrigieren, schreiben wir , um die eindeutige Zuordnung von 0 zu A zu sein , und schreiben wir e : A → 0 , um eine Zuordnung von A zu 0 zu sein .$!_A : 0 \to A$$0$$A$$e : A \to 0$$A$$0$

Nun sagt die Verteilbarkeit Bedingung , dass es ein Isomorphismus . Da ursprüngliche Objekte bis zum Isomorphismus eindeutig sind, bedeutet dies, dass A $i : 0 \simeq A \times 0$ selbst ein initiales Objekt ist. Damit können wir nun zeigen, dass A selbst ein Ausgangsobjekt ist.$A \times 0$$A$

Da ein Ausgangsobjekt ist, kennen wir die Abbildungen π 1 : A × 0 → A und ! $A \times 0$$\pi_1 : A \times 0 \to A$ sind gleich.$!_A \circ \pi_2$

Um zu zeigen, dass ein Ausgangsobjekt ist, müssen wir einen Isomorphismus zwischen A und 0 zeigen . Wählen wir e : A → 0 und ! A : 0 → A als Komponenten des Isomorphismus. Wir wollen zeigen, dass e ∘ ! A = i d 0 und ! A ∘ e = i d A .$A$$0$$e : A \to 0$$!_A : 0 \to A$$e \circ !_A = id_0$$!_A \circ e = id_A$

Zeigen, dass $e \circ !_A = id_0$ ist unmittelbar, da es nur eine Karte vom Typ gibt und wir wissen, dass es immer eine Identitätskarte gibt.$0 \to 0$

Um die andere Richtung zu zeigen, notiere

$$\begin{array}{lcll} id_A & = & \pi_1 \circ (id_A, e) & \mbox{Product equations} \\ & = & !_A \circ \pi_2 \circ (id_A, e) & \mbox{Since $A\times 0$ is initial} \\ & = & !_A \circ e & \mbox{Product equations} \end{array}$$

Wir haben also einen Isomorphismus , und so ist A ein Ausgangsobjekt. Daher sind die Abbildungen A → 0 eindeutig. Wenn Sie also e , e 'haben : A → 0 , dann ist e = e ' .$A \simeq 0$$A$$A \to 0$$e,e' : A \to 0$$e = e'$

EDIT 2: Es stellt sich heraus, dass die Situation schöner ist als ich ursprünglich dachte. Ich habe von Ulrich Bucholz gelernt, dass es offensichtlich ist (im mathematischen Sinne von "retrospektiv offensichtlich"), dass jedes biCCC distributiv ist.$\newcommand{\Hom}{\mathrm{Hom}}$ Hier ist ein süßer kleiner Beweis:

$$\begin{array}{lcl} \Hom((A + B) \times C, (A + B) \times C) & \simeq & \Hom((A + B) \times C, (A + B) \times C) \\ & \simeq & \Hom((A + B), C \to (A + B) \times C) \\ & \simeq & \Hom(A , C \to (A + B) \times C) \times \Hom(B, C \to (A + B) \times C) \\ & \simeq & \Hom(A \times C, (A + B) \times C) \times \Hom(B \times C, (A + B) \times C) \\ & \simeq & \Hom((A \times C) + (B \times C), (A + B) \times C) \end{array}$$

Die Gleichung fängt nur die Tatsache ein, dass 0 höchstens ein Element hat, also glaube ich nicht, dass Neel die ganze Geschichte einfängt . Ich würde den leeren Typ axiomatisieren$e = e' : 0$$0$ folgendermaßen.$0$

Es gibt keine Einführungsregeln. Die Eliminierungsregel ist Die Gleichung lautetmagicτ(e)=e':τwobeie:0unde':τ. Inτist jeder Typ. Die Gleichung ist wie folgt motiviert: Wenn Sie es geschafft haben, den Termmagicτ(e) zu bilden,dann ist

$$\frac{e : 0}{\mathtt{magic}_\tau(e) : \tau}.$$ $$\mathtt{magic}_\tau(e) = e' : \tau$$ $e : 0$$e' : \tau$$\tau$$\mathtt{magic}_\tau(e)$ ist bewohnt von$0$$e$, aber das ist absurd, damit alle Gleichungen gelten. Eine andere Möglichkeit, den gleichen Effekt zu erzielen, besteht darin, die Gleichung aufzustellen, die vielleicht nicht so schön ist, weil sie mit dem Kontext spielt. Andererseits zeigt es deutlicher, dass wir die Tatsache angeben, dass zwei beliebige Morphismen von 0 bis τ gleich sind (das Γ ist eine Ablenkung in einem CCC). $$x : 0, \Gamma \vdash e_1 = e_2 : \tau$$ $0$$\tau$$\Gamma$