Double Negation in Type Theory How do I derive a proof of double negation in type theory for Exercise 1.11 of the book HoTT? That is a proof of type $(((A \rightarrow \textbf{0}) \rightarrow \textbf{0}) \rightarrow \textbf{0}) \rightarrow (A \rightarrow \textbf{0})$, where objects of type $\textbf{0}$ are contradictions.
Is this equivalent to proving $((A \rightarrow \textbf{0}) \rightarrow \textbf{0}) \rightarrow A$?
 A: It is not equivalent to $((A \rightarrow \mathbf{0}) \rightarrow \mathbf{0}) \rightarrow A$; in fact, that statement (for arbitrary types $A$) is inconsistent in HoTT.
To prove $(((A \rightarrow \mathbf{0}) \rightarrow \mathbf{0}) \rightarrow \mathbf{0}) \rightarrow (A \rightarrow \mathbf{0})$ is by definition to provide a function from $((A \rightarrow \mathbf{0}) \rightarrow \mathbf{0}) \rightarrow \mathbf{0}$ and $A$ to $\mathbf{0}$—that is, a value of the form $\lambda f . \lambda a . …$.  What should go in place of the ellipses?  Well, we need a value of type $\mathbf{0}$, so it seems prudent to apply $f$ to something of type $(A \rightarrow \mathbf{0}) \rightarrow \mathbf{0}$.  In order to construct such a thing, it suffices to provide a value of the form $\lambda g . …$.  This second set of ellipses needs to be replaced with a value of type $\mathbf{0}$ again, but we now have access to $g : A \rightarrow \mathbf{0}$, so we can apply it to $a$ and we are completely done.  Consequently, a proof (and, I might add, the intended proof) of $(((A \rightarrow \mathbf{0}) \rightarrow \mathbf{0}) \rightarrow \mathbf{0}) \rightarrow (A \rightarrow \mathbf{0})$ is $\lambda f . \lambda a . f(\lambda g . g(a))$.
