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'$.

Basically, the high-level point is that not all biCCCs are models of the simply-typed lambda calculus with sums: we need to restrict our attention to the distributive biCCCs. A plain biCCC simply does have enough structure to interpret the elimination rule for sums. And if we want the empty type to be the unit for the sum type, this means that the existence of a map $A \to 0$ should mean that $A$ is itself initial.

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

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 conversion is:

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

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'$.

Basically, the high-level point is that not all biCCCs are models of the simply-typed lambda calculus with sums: we need to restrict our attention to the distributive biCCCs. A plain biCCC simply does have enough structure to interpret the elimination rule for sums. And if we want the empty type to be the unit for the sum type, this means that the existence of a map $A \to 0$ should mean that $A$ is itself initial.