<p>The equation $e = e&#39; : 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.</p>

<p>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&#39; : \tau$$ where $e : 0$ and $e&#39; : \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).</p>

CC BY-SA 3.0
2011-07-01T22:19:20.477Z
Hi Andrej, the equation you suggest is derivable from the commuting conversion I gave. $\mathtt{magic}(e) = e'$ is derivable from $C[\mathtt{magic}(e)] = \mathtt{magic}(e)$, since $\mathtt{magic}(e)$ does not actually have to occur on the left term. The analogy is to $C[\mathtt{case}(e,x.\;e',y.\;e'')] = \mathtt{case}(e, x.\;C[e'], y.\;C[e''])$, where not using the result of a case-analysis is ok if you do the same in both branches.
Neel Krishnaswami
CC BY-SA 3.0
2011-07-01T22:23:38.760Z
I should add, though, that I like the presentation with contexts better -- indeed, I think in general it's cleanest if you actually allow equations on sum values in the context! That's much nicer for actual proofs than games with commuting conversions, IMO. (IIRC, this is equivalent to adding the additional assumption of stable coproducts, but for all the models I can reasonably see caring about this holds.)
Neel Krishnaswami
CC BY-SA 3.0
2011-07-02T12:12:33.333Z
Ah yes, excellent. It was too late for me to think about commuting conversions so I pretended you did not write that part. Now Ohad can have his pick.
Andrej Bauer
CC BY-SA 3.0
2011-07-03T04:55:33.587Z
I guess the issue I taised to NeelK applies to you as well: The model class of such a ST$\lambda$C are all Bi-CCC.  The equation you gave then becomes: if one arrow $\Gamma \to \tau$ factors through the initial object then there is only one arrow $\Gamma \to \tau$. I don't see why that holds in any Bi-CCC. Does it? If not, is there a better model class I should be thinking of?
Ohad Kammar
CC BY-SA 3.0
2011-07-28T20:42:46.387Z
@Ohad: I think you want to look at the notion of a strict initial object and extensive categories (and related versions). Are you looking for a calculus that described *exactly* Bi-CCC's? What are you doing?
Andrej Bauer
CC BY-SA 3.0
2011-07-29T06:18:56.927Z
I was validating some structural ($\eta$, $\beta$, etc) rules in a class of models.  While I know the set of equations I gave wasn't complete (you need CBPV with complex values and stacks for that), I wanted to at least capture the standard equations that will be used to prove completeness if I did have enough equations.  In other words, I wanted the standard equational laws for zero types.
Ohad Kammar
CC BY-SA 3.0
2011-07-29T19:37:29.233Z
There are no standard equational laws for zero types. Logicians have always been afraid of the empty universe of discourse, and computer scientists have always been afraid of the empty type. They even named a non-empty type "void" to deny the empty type.
Andrej Bauer
CC BY-SA 3.0
2011-07-29T19:40:17.877Z
I think the difference between having a strict initial object and just an initial one is in whether you allow the equation $\mathtt{magic}_\tau(e) = e'$ in all contexts or just in the empty context. But I am half-guessing, it's just a thought.
Andrej Bauer
CC BY-SA 3.0
2011-07-01T21:43:10.363Z
2011-07-01T21:51:39.153Z
2011-07-01T21:51:39.153Z
Andrej Bauer
<ol>
<li><p>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). .</p></li>
<li><p>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: </p>

<p>$$e = \mathrm{initial}(e)$$</p>

<p>The commuting coversion is: </p>

<p>$$C[\mathrm{initial}(e)] = \mathrm{initial}(e)$$</p></li>
</ol>

<p>EDIT: </p>

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

<p>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$. </p>

<p>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. </p>

<p>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.</p>

<p>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$.</p>

<p>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.</p>

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

<p>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;$. </p>

<p>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:</p>

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

CC BY-SA 3.0
2011-07-01T16:14:01.257Z
Regarding 1: I think of a zero type as an initial object. Initial objects may have multiple arrows _into_ them, but can only have one arrow _out_ of them. In other words, I don't immediately see any reason why being bi-CCC implies 0 to be subterminal. Is there one?
Ohad Kammar
CC BY-SA 3.0
2011-07-01T16:36:17.530Z
Yes: the fact that the STLC with sums needs a *distributive* bi-CCC ($(X \times A) + (X \times B) \simeq X \times (A+B)$) to interpret it, and the uniqueness for the 0 type comes as the nullary version of that. (Try to write down the interpretation of the elimination rule for sums, and you'll see it.)
Neel Krishnaswami
CC BY-SA 3.0
2011-07-01T17:03:48.927Z
I don't follow. The distributivity amounts to $initial : 0 \to A\times 0$ having an inverse. Why does that imply that $0$ is subterminal?
Ohad Kammar
CC BY-SA 3.0
2011-07-03T21:24:53.010Z
Aha! Thanks for that proof! And for the patience, too!
Ohad Kammar
CC BY-SA 3.0
2011-07-28T10:27:43.040Z
regarding edit 2: Left adjoints preserve colimits. If the category is Cartesian closed, then $(-)\times C$ is left adjoint to $(-)^C$ so $(A+B)\times C$ **is** the sum $A\times C + B\times C$.
Ohad Kammar
CC BY-SA 3.0
2011-07-01T16:01:37.623Z
2011-07-28T07:31:42.320Z
2011-07-28T07:31:42.320Z
Neel Krishnaswami
<p><strong>Disclaimer</strong>: while I care about type theory, I don't consider myself an expert on type theory.</p>

<p>In the simply typed lambda calculus, the <strong>zero type</strong> has no constructors and a unique eliminator:</p>

<p>$$\frac{\Gamma \vdash M \colon 0}{\Gamma \vdash initial (M) \colon A}$$</p>

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

<p>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.</p>

<p>(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.)</p>

<p>So my questions are: </p>

<ol>
<li>What are the standard equational laws for zero types? </li>
<li>Are any of them classified as $\eta$ or $\beta$ laws? </li>
</ol>

<pl.programming-languages><type-theory><lambda-calculus><semantics>
What are the equational laws for zero types?
Ohad Kammar
# What are the equational laws for zero types?

(Asked by: username_0 on 2011-07-01)

**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?

**Tags:** pl.programming-languages, type-theory, lambda-calculus, semantics

---

## 2 answers

### Answer by username_2 on 2011-07-01. Score: 12 | Accepted answer

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

> **Comments:**
> **username_0**: Regarding 1: I think of a zero type as an initial object. Initial objects may have multiple arrows _into_ them, but can only have one arrow _out_ of them. In other words, I don't immediately see any reason why being bi-CCC implies 0 to be subterminal. Is there one?  
> **username_2**: Yes: the fact that the STLC with sums needs a *distributive* bi-CCC ($(X \times A) + (X \times B) \simeq X \times (A+B)$) to interpret it, and the uniqueness for the 0 type comes as the nullary version of that. (Try to write down the interpretation of the elimination rule for sums, and you'll see it.)  
> **username_0**: I don't follow. The distributivity amounts to $initial : 0 \to A\times 0$ having an inverse. Why does that imply that $0$ is subterminal?  
> **username_0**: Aha! Thanks for that proof! And for the patience, too!  
> **username_0**: regarding edit 2: Left adjoints preserve colimits. If the category is Cartesian closed, then $(-)\times C$ is left adjoint to $(-)^C$ so $(A+B)\times C$ **is** the sum $A\times C + B\times C$.  

---

### Answer by username_1 on 2011-07-01. Score: 8

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

> **Comments:**
> **username_2**: Hi Andrej, the equation you suggest is derivable from the commuting conversion I gave. $\mathtt{magic}(e) = e'$ is derivable from $C[\mathtt{magic}(e)] = \mathtt{magic}(e)$, since $\mathtt{magic}(e)$ does not actually have to occur on the left term. The analogy is to $C[\mathtt{case}(e,x.\;e',y.\;e'')] = \mathtt{case}(e, x.\;C[e'], y.\;C[e''])$, where not using the result of a case-analysis is ok if you do the same in both branches.  
> **username_2**: I should add, though, that I like the presentation with contexts better -- indeed, I think in general it's cleanest if you actually allow equations on sum values in the context! That's much nicer for actual proofs than games with commuting conversions, IMO. (IIRC, this is equivalent to adding the additional assumption of stable coproducts, but for all the models I can reasonably see caring about this holds.)  
> **username_1**: Ah yes, excellent. It was too late for me to think about commuting conversions so I pretended you did not write that part. Now Ohad can have his pick.  
> **username_0**: I guess the issue I taised to NeelK applies to you as well: The model class of such a ST$\lambda$C are all Bi-CCC.  The equation you gave then becomes: if one arrow $\Gamma \to \tau$ factors through the initial object then there is only one arrow $\Gamma \to \tau$. I don't see why that holds in any Bi-CCC. Does it? If not, is there a better model class I should be thinking of?  
> **username_1**: @Ohad: I think you want to look at the notion of a strict initial object and extensive categories (and related versions). Are you looking for a calculus that described *exactly* Bi-CCC's? What are you doing?  
> **username_0**: I was validating some structural ($\eta$, $\beta$, etc) rules in a class of models.  While I know the set of equations I gave wasn't complete (you need CBPV with complex values and stacks for that), I wanted to at least capture the standard equations that will be used to prove completeness if I did have enough equations.  In other words, I wanted the standard equational laws for zero types.  
> **username_1**: There are no standard equational laws for zero types. Logicians have always been afraid of the empty universe of discourse, and computer scientists have always been afraid of the empty type. They even named a non-empty type "void" to deny the empty type.  
> **username_1**: I think the difference between having a strict initial object and just an initial one is in whether you allow the equation $\mathtt{magic}_\tau(e) = e'$ in all contexts or just in the empty context. But I am half-guessing, it's just a thought.  

---

