<p>I already answered how to construct such terms in <a href="https://cstheory.stackexchange.com/questions/27303/what-is-a-term-of-the-type-bot-rightarrow-a">a related question</a>, so let me just amend that answer with some equations.</p>
<p>A standard type constructor which has constructors and eliminators, for instance <span class="math-container">$A \times B$</span> has pairing and projections, will have:</p>
<ul>
<li><span class="math-container">$\beta$</span>-rules which says how destructors operate on constructors, for instance: <span class="math-container">$\pi_1 (a,b) \equiv a$</span>,</li>
<li><span class="math-container">$\eta$</span>-rules which say that if we take a thing apart with destructors and put it back together we get the original thing, for instance: <span class="math-container">$(\pi_1\,u, \pi_2,u) = u$</span>.</li>
</ul>
<p>The empty type is special because it has no constructors, so where do equations come from? We can take the idea that <span class="math-container">$\mathbf{0}$</span> is the initial type and express it as an equation:
<span class="math-container">$$\mathsf{absurd}_A(e_1) \equiv_A e_2 \tag{1}$$</span>
where <span class="math-container">$\mathsf{absurd}_A : \mathbf{0} \to A$</span> is the eliminator (it could also be written as an empty case statement), <span class="math-container">$e_1 : \mathbf{0}$</span> and <span class="math-container">$e_2 : A$</span>. The equation says that <span class="math-container">$\mathsf{absurd}_A(e_1)$</span> is equal to every term of type <span class="math-container">$A$</span>, which is absurd, as it should be. The effect of the equation is that as soon as we have a variable <span class="math-container">$x : \mathbf{0}$</span> in the typing context, everything becomes trivial. In categorical language, slicing over <span class="math-container">$\mathbf{0}$</span> gives the terminal category -- which is just another way of saying that <span class="math-container">$\mathbf{0}$</span> is an initial object.</p>
<p>We can now show that every two maps <span class="math-container">$f, g : \mathbf{0} \to A$</span> are equal, simply because
<span class="math-container">$$x : \mathbf{0} \vdash f\,x \equiv \mathsf{absurd}_A(x) \equiv g\,x$$</span>
and now by congruence rule for <span class="math-container">$\lambda$</span> and <span class="math-container">$\eta$</span>-rule for functions
<span class="math-container">$$f \equiv (\lambda x : \mathbf{0} \,.\, f\,x) \equiv (\lambda x : \mathbf{0} \,.\, g\,x) \equiv g.$$</span>
Note however that (1) above is not the kind of equation that type theorists like, because it screwes up various algorithms for checking equality of terms.</p>

CC BY-SA 4.0
2014-12-02T09:26:37.650Z
2021-08-26T10:15:38.577Z
2021-08-26T10:15:38.577Z
Andrej Bauer
<p>In a plain type theory with just dependent functions and a universe, you can define:</p>
<p><span class="math-container">$$
\textbf 0 \equiv (A: \textrm{Type}) \rightarrow (B: \textrm{Type}) \rightarrow A \rightarrow B
$$</span></p>
<p>Then you get a map:
<span class="math-container">$$
\textrm{0m} : (X: \textrm{Type}) \rightarrow \textbf 0 \rightarrow X
$$</span>
<span class="math-container">$$
\textrm{0m}\,\, X\,\, z\, \equiv z\,\, \textbf 0\,\, X\,\, z
$$</span></p>
<p><strong>Note:</strong> This definition is impredicative, and thus requires some kind of super universe or other means to avoid Girard's paradox.</p>

CC BY-SA 4.0
2021-08-29T12:22:42.147Z
Thanks. How's the bracketing in "$\ 0\ \ $"? I don't quite understand the role of passing something to $z$.
Nikolaj-K
CC BY-SA 4.0
2021-08-30T18:19:24.350Z
@Nikolaj-K Since $\textbf 0$ is really a function type, $z : \textbf 0$ is a function taking 3 parameters. Thus, we pass it 2 types and a term of the 1st type (as per the signature). The bracketing works as in Haskell, left associativity of calls.
DrunkCoder
CC BY-SA 4.0
2021-09-03T18:27:48.483Z
IMO normally we name $0m$ as 'absurd' or $\bot\text{-elim}$ or something. Did you invent the name yourself, or is it borrowed somewhere else?
ice1000
CC BY-SA 4.0
2021-09-06T17:41:56.747Z
@ice1000 Yeah, I use it in my notes (as an abbreviation of "0 map"), and I have subcosciously used it here. Should I edit the answer?
DrunkCoder
CC BY-SA 4.0
2021-08-28T21:37:17.390Z
2021-08-28T21:37:17.390Z
DrunkCoder
<p>If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we have the <a href="http://en.wikipedia.org/wiki/Empty_function" rel="nofollow">empty function</a> in $\emptyset\to A$. This makes $\emptyset$ the initial object in the category of sets. By set extensionality, there is only this empty function and this also fits with cardinalities, where we like $|A^{\emptyset}|=|A|^{|\emptyset|}=1$.
In logic, we usually take that form absurdum follows everything, ex falso quodlibet, and in the propositions interpretation for types, if $\bf 0$ denotes the empty type (or bottom type), we want a function ${\bf 0}\to \tau$ for all types $\tau$ too.</p>

<p>I've been told in some programs this would be done by defining alla</p>

<p>definition exfalso (a : Type) (x : 0) : a := "case x of -emptyspace-"</p>

<p>Now I try to construct the terms for function types involving the empty type over the standard theories you'd find in books, but I can't quite reproduce the good properties, see below. I wonder</p>

<blockquote>
  <p>Which type theories actually let you <em>construct</em> a term of a function type from the empty type, and then, is it unique?</p>
</blockquote>

<p>My considerations (leading to more question) are this...</p>

<p>Take <a href="http://en.wikipedia.org/wiki/Simply-typed_lambda_calculus#Typing_rules" rel="nofollow">simply types lambda calculus</a>. We have $(\lambda (x:\tau).x):\tau\to\tau$ and so $(\lambda (x:{\bf 0}).x):{\bf 0}\to{\bf 0}$. In any model of the type theory, this will be the empty function and so I'm okay with that. But how do I construct, from the typing rules of the theory, any type of ${\bf 0}\to{\bf \tau}$, where $\tau$ isn't ${\bf 0}$? And then, how is there only one? Depending on how the theory lets you define functions, I could imagine ${\bf 0}\to\mathrm{Nat}$ to have zero or an infinite number of terms (constant functions which can never take any input). I guess the cardinal arithmetic then only works out once we pass to the set theoretic model, where all those constant functions are, extensionally, the empty function. Is that right? In a type theory with booleans $\bf 2$, how many functions $\bf 0\to\bf 2$ are there? If $a,b:\bf 2$, are $\lambda x.a$ and $\lambda x.b$ generally two function of this type?</p>

CC BY-SA 3.0
2014-11-30T20:33:53.950Z
You need to be careful what kind of equality you have in mind when answering the question how many functions of type  $\mathbf{0} \rightarrow \tau$ there are: syntactically e.g. $f = \lambda x^{\mathbf{0}}.3$ and $g = \lambda x^{\mathbf{0}}.17$ are distinct, but for extensional equalities $\cong$ they are equal, since for all inhabitants $M$ of $\mathbf{0}$ we have $fM \cong gM$.
Martin Berger
CC BY-SA 3.0
2014-12-02T09:10:20.830Z
Related question: http://cstheory.stackexchange.com/questions/27303/what-is-a-term-of-the-type-bot-rightarrow-a
Andrej Bauer
CC BY-SA 3.0
2014-12-02T09:40:01.907Z
@MartinBerger, you still need to axiomatize *something* about $\mathbf{0}$ to be able to conclude that "for all inhabitants $M$ of $\mathbf{0}$ we have $f M \equiv g M$". And when you do, if you do it right, you don't need function extensionality, see my answer.
Andrej Bauer
CC BY-SA 3.0
2014-12-02T09:55:31.223Z
@AndrejBauer Why do you need the equality (1) in your answer for something like $\lambda x^{\mathbf{0}}.17$? That term does not make use of $\mathsf{absurd}_A(E)$. All you need here is that $\mathsf{0}$ has no inhabitants.
Martin Berger
CC BY-SA 3.0
2014-12-02T10:28:05.507Z
But how do you say "$\mathbf{0}$ has no inhabitants" in a type theory? Just because there is no constructor for $\mathbf{0}$ that does not mean you can actually use the fact that there are no inhabitants. You need an axiom somewhere. I used it to show that $f x$ and $g x$ are equal. Or to put it another way: how will you derive (using function extensionality if you wish) that any two functions $\mathbf{0} \to A$ are extensionally equal? I am *not* talking about a meta-theorem of the form "every two closed terms of type $\mathbf{0} \to A$ are equal", that's the wrong theorem to prove.
Andrej Bauer
CC BY-SA 3.0
2014-12-02T14:15:11.457Z
@AndrejBauer I was in fact thinking of a meta-theorem showing that $\mathbf{0}$ has no inhabitants.
Martin Berger
CC BY-SA 3.0
2014-12-02T14:34:28.257Z
Yes, I deduced that from the fact that you thought no additional axioms were necessary :-) But I claim that's not "the correct" theorem because it gives people the wrong idea. The theorem "there are no closed terms of $\mathbf{0}$" translates semantically to "there is no morphism $\mathbf{1} \to \mathbf{0}$" which is very much *not* equivalent to "$\mathbf{0}$ is initial" (as we both know very well). So from an educational point of view I'd hide such a meta-theorem in a closet, or at least decorate it with a caveat.
Andrej Bauer
<type-theory><lambda-calculus><function>
Constructing terms of function types out of the empty type
Nikolaj-K
# Constructing terms of function types out of the empty type

(Asked by: username_0 on 2014-11-30)

If a function $f$ is understood as its graph, i.e. a set of pairs $\langle x,y\rangle$ where $x$ is input and $y$ is output, then the empty set $\emptyset$ is a valid function, and for any set $A$, we have the [empty function](http://en.wikipedia.org/wiki/Empty_function) in $\emptyset\to A$. This makes $\emptyset$ the initial object in the category of sets. By set extensionality, there is only this empty function and this also fits with cardinalities, where we like $|A^{\emptyset}|=|A|^{|\emptyset|}=1$.
In logic, we usually take that form absurdum follows everything, ex falso quodlibet, and in the propositions interpretation for types, if $\bf 0$ denotes the empty type (or bottom type), we want a function ${\bf 0}\to \tau$ for all types $\tau$ too.

I've been told in some programs this would be done by defining alla

definition exfalso (a : Type) (x : 0) : a := "case x of -emptyspace-"

Now I try to construct the terms for function types involving the empty type over the standard theories you'd find in books, but I can't quite reproduce the good properties, see below. I wonder

> Which type theories actually let you *construct* a term of a function type from the empty type, and then, is it unique?

My considerations (leading to more question) are this...

Take [simply types lambda calculus](http://en.wikipedia.org/wiki/Simply-typed_lambda_calculus#Typing_rules). We have $(\lambda (x:\tau).x):\tau\to\tau$ and so $(\lambda (x:{\bf 0}).x):{\bf 0}\to{\bf 0}$. In any model of the type theory, this will be the empty function and so I'm okay with that. But how do I construct, from the typing rules of the theory, any type of ${\bf 0}\to{\bf \tau}$, where $\tau$ isn't ${\bf 0}$? And then, how is there only one? Depending on how the theory lets you define functions, I could imagine ${\bf 0}\to\mathrm{Nat}$ to have zero or an infinite number of terms (constant functions which can never take any input). I guess the cardinal arithmetic then only works out once we pass to the set theoretic model, where all those constant functions are, extensionally, the empty function. Is that right? In a type theory with booleans $\bf 2$, how many functions $\bf 0\to\bf 2$ are there? If $a,b:\bf 2$, are $\lambda x.a$ and $\lambda x.b$ generally two function of this type?

**Tags:** type-theory, lambda-calculus, function
> **Comments:**
> **username_1**: You need to be careful what kind of equality you have in mind when answering the question how many functions of type  $\mathbf{0} \rightarrow \tau$ there are: syntactically e.g. $f = \lambda x^{\mathbf{0}}.3$ and $g = \lambda x^{\mathbf{0}}.17$ are distinct, but for extensional equalities $\cong$ they are equal, since for all inhabitants $M$ of $\mathbf{0}$ we have $fM \cong gM$.  
> **username_2**: Related question: http://cstheory.stackexchange.com/questions/27303/what-is-a-term-of-the-type-bot-rightarrow-a  
> **username_2**: @MartinBerger, you still need to axiomatize *something* about $\mathbf{0}$ to be able to conclude that "for all inhabitants $M$ of $\mathbf{0}$ we have $f M \equiv g M$". And when you do, if you do it right, you don't need function extensionality, see my answer.  
> **username_1**: @AndrejBauer Why do you need the equality (1) in your answer for something like $\lambda x^{\mathbf{0}}.17$? That term does not make use of $\mathsf{absurd}_A(E)$. All you need here is that $\mathsf{0}$ has no inhabitants.  
> **username_2**: But how do you say "$\mathbf{0}$ has no inhabitants" in a type theory? Just because there is no constructor for $\mathbf{0}$ that does not mean you can actually use the fact that there are no inhabitants. You need an axiom somewhere. I used it to show that $f x$ and $g x$ are equal. Or to put it another way: how will you derive (using function extensionality if you wish) that any two functions $\mathbf{0} \to A$ are extensionally equal? I am *not* talking about a meta-theorem of the form "every two closed terms of type $\mathbf{0} \to A$ are equal", that's the wrong theorem to prove.  
> **username_1**: @AndrejBauer I was in fact thinking of a meta-theorem showing that $\mathbf{0}$ has no inhabitants.  
> **username_2**: Yes, I deduced that from the fact that you thought no additional axioms were necessary :-) But I claim that's not "the correct" theorem because it gives people the wrong idea. The theorem "there are no closed terms of $\mathbf{0}$" translates semantically to "there is no morphism $\mathbf{1} \to \mathbf{0}$" which is very much *not* equivalent to "$\mathbf{0}$ is initial" (as we both know very well). So from an educational point of view I'd hide such a meta-theorem in a closet, or at least decorate it with a caveat.  

---

## 2 answers

### Answer by username_2 on 2014-12-02. Score: 2 | Accepted answer

I already answered how to construct such terms in [a related question](https://cstheory.stackexchange.com/questions/27303/what-is-a-term-of-the-type-bot-rightarrow-a), so let me just amend that answer with some equations.

A standard type constructor which has constructors and eliminators, for instance $A \times B$ has pairing and projections, will have:

* $\beta$-rules which says how destructors operate on constructors, for instance: $\pi\_1 (a,b) \equiv a$,
* $\eta$-rules which say that if we take a thing apart with destructors and put it back together we get the original thing, for instance: $(\pi\_1\,u, \pi\_2,u) = u$.

The empty type is special because it has no constructors, so where do equations come from? We can take the idea that $\mathbf{0}$ is the initial type and express it as an equation:
$$\mathsf{absurd}\_A(e\_1) \equiv\_A e\_2 \tag{1}$$
where $\mathsf{absurd}\_A : \mathbf{0} \to A$ is the eliminator (it could also be written as an empty case statement), $e\_1 : \mathbf{0}$ and $e\_2 : A$. The equation says that $\mathsf{absurd}\_A(e\_1)$ is equal to every term of type $A$, which is absurd, as it should be. The effect of the equation is that as soon as we have a variable $x : \mathbf{0}$ in the typing context, everything becomes trivial. In categorical language, slicing over $\mathbf{0}$ gives the terminal category -- which is just another way of saying that $\mathbf{0}$ is an initial object.

We can now show that every two maps $f, g : \mathbf{0} \to A$ are equal, simply because
$$x : \mathbf{0} \vdash f\,x \equiv \mathsf{absurd}\_A(x) \equiv g\,x$$
and now by congruence rule for $\lambda$ and $\eta$-rule for functions
$$f \equiv (\lambda x : \mathbf{0} \,.\, f\,x) \equiv (\lambda x : \mathbf{0} \,.\, g\,x) \equiv g.$$
Note however that (1) above is not the kind of equation that type theorists like, because it screwes up various algorithms for checking equality of terms.


---

### Answer by username_3 on 2021-08-28. Score: 1

In a plain type theory with just dependent functions and a universe, you can define:

$$
\textbf 0 \equiv (A: \textrm{Type}) \rightarrow (B: \textrm{Type}) \rightarrow A \rightarrow B
$$

Then you get a map:
$$
\textrm{0m} : (X: \textrm{Type}) \rightarrow \textbf 0 \rightarrow X
$$
$$
\textrm{0m}\,\, X\,\, z\, \equiv z\,\, \textbf 0\,\, X\,\, z
$$

**Note:** This definition is impredicative, and thus requires some kind of super universe or other means to avoid Girard's paradox.

> **Comments:**
> **username_0**: Thanks. How's the bracketing in "$\ 0\ \ $"? I don't quite understand the role of passing something to $z$.  
> **username_3**: @Nikolaj-K Since $\textbf 0$ is really a function type, $z : \textbf 0$ is a function taking 3 parameters. Thus, we pass it 2 types and a term of the 1st type (as per the signature). The bracketing works as in Haskell, left associativity of calls.  
> **username_4**: IMO normally we name $0m$ as 'absurd' or $\bot\text{-elim}$ or something. Did you invent the name yourself, or is it borrowed somewhere else?  
> **username_3**: @ice1000 Yeah, I use it in my notes (as an abbreviation of "0 map"), and I have subcosciously used it here. Should I edit the answer?  

---

