What are the equational laws for zero types? 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&#39; \colon 0$, then : $M = M&#39;$. 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: 


What are the standard equational laws for zero types? 
Are any of them classified as $\eta$ or $\beta$ laws?
The standard equational rules for the empty type is, as you surmise, $\Gamma \vdash e = e&#39; : 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&#39; : \Gamma \to 0$ must also be equal, since they have a common graph (namely, the empty graph). .
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 &amp; = &amp; \pi_1 \circ (id_A, e) &amp; \mbox{Product equations} \\
       &amp; = &amp; !_A \circ \pi_2 \circ (id_A, e) &amp; \mbox{Since $A\times 0$ is initial} \\
       &amp; = &amp; !_A \circ e &amp; \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&#39; : A \to 0$, then $e = e&#39;$. 

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) 
   &amp; \simeq &amp; \Hom((A + B) \times C, (A + B) \times C) \\
   &amp; \simeq &amp; \Hom((A + B), C \to (A + B) \times C) \\
   &amp; \simeq &amp; \Hom(A , C \to (A + B) \times C) \times \Hom(B, C \to (A + B) \times C) \\
   &amp; \simeq &amp; \Hom(A \times C, (A + B) \times C) \times \Hom(B \times C, (A + B) \times C) \\
   &amp; \simeq &amp; \Hom((A \times C) + (B \times C), (A + B) \times C)
\end{array}
$$