Type theoretic proof that $\lnot (A \lor B) \Rightarrow \lnot A \land \lnot B$ I'm currently giving the Homotopy Type Theory book a go, and have made it to the section (of Chapter 1) on Propositions as Types. It leaves as an exercise for the reader the proof that $$ ((A + B)\to 0) \to (A \to 0)\times (B \to 0)$$ which I understand to mean define $f: ((A + B)\to 0) \to (A \to 0)\times (B \to 0)$ for any $A$, $B$. As far as I can tell the function $\lambda g.(g(inr(a), g(inl(b)))$ should do the trick. Does it? Does simply constructing that function constitute a proof? 
I'm not entirely sure if I understand how functions work in this theory, nor definitions, nor proofs so if this is obviously true or blatantly false please let me know. It would hopefully go some way towards me getting a clearer picture in mind mind.
(Edit) What I had meant to say was $\lambda g.(\lambda a.g(inr(a), \lambda b.g(inl(b)))$, as the answers have pointed out.
 A: Yes, merely writing a well-typed program with the appropriate type constitutes a proof when you're using a type theory (kinda fun no?).
As far as your specific example though your proof isn't quite right. You know that the general shape must be $\lambda x. \_$ because you're producing a pi-type, but your codomain is supposed to be a pair of functions. Yours makes references to these $a$ and $b$ variables which seem to spring from no where. You'd want something more like
$$\lambda g.\ (\lambda a.\ M, \lambda b.\ N)$$
where $M$ and $N$ are of type $0$ and may $g$. I'll leave it to you to fill in what exactly they should be since it's a good exercise and you're very close.
A: Your solution is almost correct: to be exact the problem is that in defining the element of type 
$$((A + B) \to 0) \to (A \to 0) \times (B \to 0)$$
you make use of two terms $a$ and $b$ which are not defined.
Nevertheless the road is correct, you have to simply provide a term of the given type to prove that type-proposition.
A correct solution is 
$$\lambda g.\left(\lambda a.g(inl(a)),\lambda b.g(inr(b))\right)$$
or if you prefer 
$\lambda g.(g \circ inl,g \circ inr)$, where $inl$ and $inr$ are embedding in $A+B$.
