# Proving a proposition by inhabiting a type

I am working through HoTT and it was suggested (on page 43) that the reader prove the following proposition, if not(A or B) then (not A) and (not B) by exhibiting an element of the type $$(A+B \to 0) \to (A\to 0) \times (B \to 0)$$. Introduce the variable (or hypothesis) $$g: A+B \to 0$$. We need to form an expression $$f(g) :\equiv \box : (A \to 0) \times (B \to 0)$$. (I do not know the command for the box used in HoTT which is the expression we are trying to fill.) No with a function $$g:A+B \to 0$$ we implicitly have $$g_0 : A \to B$$ and $$g_1 : B \to 0$$ such that $$g(inl(a)) \equiv g_0(a)$$ and $$g(inr(b)) \equiv g_1(b)$$. So, we clearly can define $$f(g) :\equiv (g_0,g_1)$$.

How do I define $$f$$ explicitly? It feels wrong saying $$f :\equiv \lambda g. (g_0,g_1)$$. I assume I should use the recursor as was suggested in the converse direction which the preceeding paragraph works through.

Note that, if $$g$$ is of type $$A+B\to 0$$, then $$\lambda a.g(\mathrm{inl}(a))$$ is of type $$A\to 0$$ and $$\lambda b.g(\mathrm{inr}(b))$$ is of type $$B\to 0$$. (These are what you refer to as $$g_0$$ and $$g_1$$ in your post.) So the term $$\lambda g.(\lambda a.g(\mathrm{inl}(a)),\lambda b.g(\mathrm{inr}(b)))$$ is of type $$(A+B\to 0)\to\left[(A\to 0)\times(B\to 0)\right]$$.