¿Cuáles son las leyes equitativas para los tipos cero?

Descargo de responsabilidad : aunque me importa la teoría de tipos, no me considero un experto en teoría de tipos.

En el cálculo lambda de tipo simple, el tipo cero no tiene constructores y un eliminador único:

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

Desde un punto de vista denotacional, la ecuación es obvia (cuando los tipos tienen sentido).$initial (M_1) = initial(M_2)$

Sin embargo, desde esa perspectiva también puedo deducir que, cuando , entonces: . Esta deducción parece más fuerte, aunque un modelo particular que lo muestra se me escapa.M = M $M,M' \colon 0$$M = M'$

(Sin embargo, tengo cierta intuición teórica de la prueba: no importa qué contradicción uses para obtener un habitante, pero puede haber diferentes pruebas de contradicción).

Entonces mis preguntas son:

1. ¿Cuáles son las leyes equitativas estándar para los tipos cero?
2. ¿Alguno de ellos está clasificado como leyes $\eta$ o $\beta$ ?

1. Las reglas de ecuación estándar para el tipo vacío son, como supones, . Piense en el modelo estándar de teoría de conjuntos, donde los conjuntos se interpretan por tipos: los tipos de suma son uniones disjuntas, y el tipo vacío es el conjunto vacío. Entonces, cualquiera de las dos funciones e , e ' : Γ → 0 también debe ser igual, ya que tienen un gráfico común (es decir, el gráfico vacío). .$\Gamma \vdash e = e' : 0$$e,e' : \Gamma \to 0$

2. El tipo vacío no tiene reglas , ya que no hay formas de introducción para ello. Su única regla de ecuación es una regla η . Sin embargo, dependiendo de cuán estrictamente desee interpretar qué es una regla eta, puede desglosar esto en η más una conversión de conmutación. La estricta regla η es:$\beta$$\eta$$\eta$$\eta$

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

   La cobertura de los desplazamientos es:

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

EDITAR:

He aquí por qué la distributividad en el tipo cero implica la igualdad de todos los mapas .$A \to 0$

Para arreglar la notación, escriba ! A : 0 → A para ser el mapa único de 0 a A , y escriba e : A → 0 para que sea un mapa de A a 0 .$!_A : 0 \to A$$0$$A$$e : A \to 0$$A$$0$

Ahora, la condición de distributividad dice que hay un isomorfismo . Dado que los objetos iniciales son únicos hasta el isomorfismo, esto significa que A × 0 es en sí mismo un objeto inicial. Ahora podemos usar esto para mostrar que A en sí es un objeto inicial.$i : 0 \simeq A \times 0$$A \times 0$$A$

Como es un objeto inicial, conocemos los mapas π 1 : A × 0 → A y ! A ∘ π 2 son iguales.$A \times 0$$\pi_1 : A \times 0 \to A$$!_A \circ \pi_2$

Ahora, para mostrar que es un objeto inicial, necesitamos mostrar un isomorfismo entre él y 0 . ¡Elija e : A → 0 y ! A : 0 → A como los componentes del isomorfismo. Queremos mostrar que e ∘ ! A = i d 0 y ! 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$

Mostrando que es inmediato, ya que solo hay un mapa de tipo 0 → 0 , y sabemos que siempre hay un mapa de identidad.$e \circ !_A = id_0$$0 \to 0$

Para mostrar la otra dirección, tenga en cuenta que

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

Por lo tanto, tenemos un isomorfismo , por lo que A es un objeto inicial. Por lo tanto, los mapas A → 0 son únicos, y si tiene e , e ′ : A → 0 , entonces e = e ′ .$A \simeq 0$$A$$A \to 0$$e,e' : A \to 0$$e = e'$

EDIT 2: Resulta que la situación es más bonita de lo que pensaba originalmente. Aprendí de Ulrich Bucholz que es obvio (en el sentido matemático de "obvio retrospectivamente") que cada biCCC es distributivo.$\newcommand{\Hom}{\mathrm{Hom}}$ Aquí hay una pequeña prueba linda:

$$\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}.$$ $$\mathtt{magic}_\tau(e) = e' : \tau$$ $e : 0$$e' : \tau$$\tau$$\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).