Quais são as leis equacionais para zero tipos?

Isenção de responsabilidade : enquanto me preocupo com a teoria dos tipos, não me considero um especialista em teoria dos tipos.

No cálculo lambda de digitação simples, o tipo zero não possui construtores e um eliminador exclusivo:

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

De um ponto de vista denotacional, a equação $initial (M_1) = initial(M_2)$ é óbvio (quando os tipos sentido).

Contudo, dessa perspectiva, também posso deduzir que, quando $M,M' \colon 0$ , então: $M = M'$ . Essa dedução parece mais forte, embora um modelo específico que a mostre me ilude.

(Contudo, tenho alguma intuição teórica da prova: não importa qual contradição você usa para obter um habitante, mas pode haver diferentes provas de contradição.)

Então, minhas perguntas são:

1. Quais são as leis equacionais padrão para os tipos zero?
2. Algum deles é classificado como leis $\eta$ ou $\beta$ ?

1. As regras equacionais padrão para o tipo vazio são, como você supõe, . Pense no modelo padrão da teoria dos conjuntos, em que os conjuntos são interpretados por tipos: os tipos de soma são uniões disjuntas e o tipo vazio é o conjunto vazio. Portanto, quaisquer duas funções e , e ' : Γ → 0 também devem ser iguais, pois possuem um gráfico comum (ou seja, o gráfico vazio). .$\Gamma \vdash e = e' : 0$$e,e' : \Gamma \to 0$

2. O tipo vazio não possui regras , pois não há formas de introdução para ele. Sua única regra equacional é uma regra- η . No entanto, dependendo de quão estritamente você deseja interpretar o que é uma eta-regra, você pode dividir isso em η mais uma conversão pendular. A regra η estrita é:$\beta$$\eta$$\eta$$\eta$

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

   A cobertura pendular é:

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

EDITAR:

$A \to 0$

$!_A : 0 \to A$$0$$A$$e : A \to 0$$A$$0$

$i : 0 \simeq A \times 0$$A \times 0$$A$

$A \times 0$$\pi_1 : A \times 0 \to A$$!_A \circ \pi_2$

$A$$0$$e : A \to 0$$!_A : 0 \to A$$e \circ !_A = id_0$$!_A \circ e = id_A$

$e \circ !_A = id_0$$0 \to 0$

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

$A \simeq 0$$A$$A \to 0$$e,e' : A \to 0$$e = e'$

EDIT 2: Acontece que a situação é mais bonita do que eu pensava originalmente. Aprendi com Ulrich Bucholz que é óbvio (no sentido matemático de "retrospectivamente óbvio") que todo biCCC é distributivo.$\newcommand{\Hom}{\mathrm{Hom}}$ Aqui está uma pequena prova:

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

$e = e' : 0$$0$$0$

$$\frac{e : 0}{\mathtt{magic}_\tau(e) : \tau}.$$ $$\mathtt{magic}_\tau(e) = e' : \tau$$ $e : 0$$e' : \tau$$\tau$$\mathtt{magic}_\tau(e)$$0$$e$ $$x : 0, \Gamma \vdash e_1 = e_2 : \tau$$ $0$$\tau$$\Gamma$