Constructing terms of function types out of the empty type
I already answered how to construct such terms in a related question, 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 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.