Apa hukum persamaan untuk tipe nol?

Penafian : sementara saya peduli tentang teori jenis, saya tidak menganggap diri saya ahli dalam teori jenis.

Dalam kalkulus lambda yang diketik sederhana, tipe nol tidak memiliki konstruktor dan eliminator unik:

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

Dari sudut pandang denotasional, persamaan jelas (ketika jenisnya masuk akal).$initial (M_1) = initial(M_2)$

Namun, dari perspektif itu saya juga dapat menyimpulkan bahwa, ketika , maka: M = M ′ . Pengurangan ini tampaknya lebih kuat, meskipun model tertentu yang menunjukkannya tidak bisa saya dapatkan.$M,M' \colon 0$$M = M'$

(Saya punya beberapa intuisi teori-bukti: tidak masalah kontradiksi yang Anda gunakan untuk mendapatkan penghuni, tetapi mungkin ada bukti kontradiksi yang berbeda.)

Jadi pertanyaan saya adalah:

1. Apa hukum persamaan standar untuk tipe nol?
2. Apakah ada yang diklasifikasikan sebagai hukum atau β ?$\eta$$\beta$

1. Aturan persamaan standar untuk tipe kosong adalah, seperti yang Anda duga, . Pikirkan model set-theoretic standar, di mana set diinterpretasikan berdasarkan tipe: tipe penjumlahan adalah serikat yang terpisah, dan tipe kosong adalah set kosong. Jadi setiap dua fungsi e , e ′ : Γ → 0 juga harus sama, karena mereka memiliki grafik yang sama (yaitu, grafik kosong). .$\Gamma \vdash e = e' : 0$$e,e' : \Gamma \to 0$

2. Jenis kosong tidak memiliki aturan , karena tidak ada formulir pengantar untuk itu. Satu-satunya aturan persamaannya adalah aturan- η . Namun, tergantung pada seberapa ketat Anda ingin menafsirkan apa itu aturan eta, Anda dapat memecahnya menjadi η plus konversi komuter. Aturan η yang ketat adalah:$\beta$$\eta$$\eta$$\eta$

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

   Penutup komuter adalah:

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

EDIT:

Inilah mengapa distribusi pada tipe nol menyiratkan kesetaraan semua peta .$A \to 0$

Untuk memperbaiki notasi, mari menulis menjadi peta unik dari 0 hingga A , dan mari kita tulis e : A → 0 untuk menjadi beberapa peta dari A hingga 0 .$!_A : 0 \to A$$0$$A$$e : A \to 0$$A$$0$

Sekarang, kondisi distribusi mengatakan bahwa ada isomorfisme . Karena objek awal unik hingga isomorfisma, ini berarti bahwa A × 0 sendiri merupakan objek awal. Kita sekarang dapat menggunakan ini untuk menunjukkan bahwa A itu sendiri adalah objek awal.$i : 0 \simeq A \times 0$$A \times 0$$A$

Karena adalah objek awal, kita tahu peta π 1 : A × 0 → A dan ! A ∘ π 2 sama.$A \times 0$$\pi_1 : A \times 0 \to A$$!_A \circ \pi_2$

Sekarang, untuk menunjukkan bahwa adalah objek awal, kita perlu menunjukkan isomorfisme antara itu dan 0 . Mari kita pilih e : A → 0 dan ! A : 0 → A sebagai komponen isomorfisme. Kami ingin menunjukkan bahwa e ∘ ! A = i d 0 dan ! Sebuah ∘ e = i d A .$A$$0$$e : A \to 0$$!_A : 0 \to A$$e \circ !_A = id_0$$!_A \circ e = id_A$

Menunjukkan langsung, karena hanya ada satu peta tipe 0 → 0 , dan kita tahu bahwa selalu ada peta identitas.$e \circ !_A = id_0$$0 \to 0$

Untuk menunjukkan arah lain, catat

$$\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}$$

Karenanya kita memiliki isomorfisme , dan A adalah objek awal. Karenanya peta A → 0 unik, dan jadi jika Anda memiliki e , e ′ : A → 0 , maka e = e ′ .$A \simeq 0$$A$$A \to 0$$e,e' : A \to 0$$e = e'$

EDIT 2: Ternyata situasinya lebih cantik dari yang saya kira sebelumnya. Saya belajar dari Ulrich Bucholz bahwa sudah jelas (dalam pengertian matematika "jelas secara retrospektif") bahwa setiap biCCC bersifat distributif.$\newcommand{\Hom}{\mathrm{Hom}}$ Ini bukti kecil yang lucu:

$$\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}$$

The equation $e = e' : 0$ only captures the fact that $0$ has at most one element so I don't think Neel is capturing the whole story. I would axiomatize the empty type $0$ as follows.

There are no introduction rules. The elimination rule is

$$\frac{e : 0}{\mathtt{magic}_\tau(e) : \tau}.$$ The equation is $$\mathtt{magic}_\tau(e) = e' : \tau$$ where $e : 0$ and $e' : \tau$. Throughout $\tau$ is any type. The equation is motivated as follows: if you managed to form the term $\mathtt{magic}_\tau(e)$ then $0$ is inhabited by $e$, but this is absurd so all equations hold. So another way of achieving the same effect would be to pose the equation $$x : 0, \Gamma \vdash e_1 = e_2 : \tau$$ which is perhaps not so nice because it fiddles with the context. On the other hand, it shows more clearly that we are stating the fact that any two morphisms from $0$ to $\tau$ are equal (the $\Gamma$ is a distraction in a CCC).