What are the equational laws for zero types?

Question

Disclaimer: while I care about type theory, I don't consider myself an expert on type theory.

In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator:

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

From a denotational point of view, the equation $initial (M_1) = initial(M_2)$ is obvious (when the types make sense).

However, from that perspective I can also deduce that, when $M,M' \colon 0$, then : $M = M'$. This deduction seems stronger, although a particular model that shows it eludes me.

(I have some proof-theoretic intuition though: it doesn't matter which contradiction you use to obtain an inhabitant, but there might be different contradiction proofs.)

So my questions are:

1. What are the standard equational laws for zero types?
2. Are any of them classified as $\eta$ or $\beta$ laws?

Answer 1

1. The standard equational rules for the empty type is, as you surmise, $\Gamma \vdash e = e' : 0$. Think of the standard set-theoretic model, where sets are interpreted by types: sum types are disjoint unions, and the empty type is the empty set. So any two functions $e,e' : \Gamma \to 0$ must also be equal, since they have a common graph (namely, the empty graph). .

2. The empty type has no $\beta$ rules, since there are no introduction forms for it. Its only equational rule is an $\eta$-rule. However, depending on how strictly you wish to interpret what an eta-rule is, you may wish break this down into an $\eta$ plus a commuting conversion. The strict $\eta$-rule is:

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

   The commuting coversion is:

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

EDIT:

Here's why distributivity at the zero type implies the equality of all maps $A \to 0$.

To fix notation, let's write $!_A : 0 \to A$ to be the unique map from $0$ to $A$, and let's write $e : A \to 0$ to be some map from $A$ to $0$.

Now, the distributivity condition says that there's an isomorphism $i : 0 \simeq A \times 0$. Since initial objects are unique up to isomorphism, this means that $A \times 0$ is itself a initial object. We can now use this to show that $A$ itself is an initial object.

Since $A \times 0$ is an initial object, we know the maps $\pi_1 : A \times 0 \to A$ and $!_A \circ \pi_2$ are equal.

Now, to show that $A$ is an initial object, we need to show an isomorphism between it and $0$. Let's choose $e : A \to 0$ and $!_A : 0 \to A$ as the components of the isomorphism. We want to show that $e \circ !_A = id_0$ and $!_A \circ e = id_A$.

Showing that $e \circ !_A = id_0$ is immediate, since there is only one map of type $0 \to 0$, and we know that there is always an identity map.

To show the other direction, note $$ \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} $$

Hence we have an isomorphism $A \simeq 0$, and so $A$ is an initial object. Therefore maps $A \to 0$ are unique, and so if you have $e,e' : A \to 0$, then $e = e'$.

EDIT 2: It turns out the situation is prettier than I originally thought. I learned from Ulrich Bucholz that it's obvious (in the mathematical sense of "retrospectively obvious") that every biCCC is distributive. $\newcommand{\Hom}{\mathrm{Hom}}$ Here's a cute little proof:

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

Answer 2

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).