# Constructing terms of function types out of the empty type

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

• 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 Nov 30 '14 at 20:33
• Related question: cstheory.stackexchange.com/questions/27303/… – Andrej Bauer Dec 2 '14 at 9:10
• @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 Dec 2 '14 at 9:40
• @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 Dec 2 '14 at 9:55
• 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 Dec 2 '14 at 10:28

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 a terminal 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.