Type Theory: we cannot prove double negation, but can we prove it is unprovable?

Question

I'm currently trying to learn type theory from the first chapter of HoTT. It is remarked that we cannot prove $\neg\neg A \rightarrow A$, when $A$ is interpreted as a proposition, or, equivalently, we cannot construct an element of $((A\rightarrow\mathbf{0})\rightarrow \mathbf{0})\rightarrow A$, when $A$ is interpreted as a type. However, can we prove from within type theory that this is unprovable? In other words, can we construct an element of the following type?

$$\Bigg(\prod_{A:\mathcal{U}} \big(((A\rightarrow\mathbf{0})\rightarrow \mathbf{0})\rightarrow A\big)\Bigg)\rightarrow \mathbf{0}$$

If so, what is such an element? I've been struggling to explicitly construct one myself, to no avail.

Answer 1

As @DanDoel noticed, you can construct an element of $\big(\prod_{A:U}(\neg\neg A\to A)\big)\to \mathbb{0}$, this is Theorem 3.2.2 of the HoTT book.

If you restrict it to propositions, $\prod_{A:U}\big(\text{isProp}(A)\to(\neg\neg A\to A)\big)$ is the law of double negation, and is equivalent to the law of excluded middle LEM.

It is not possible to prove LEM in HoTT, but it can be admitted as an axiom, so $\text{LEM}\to \mathbb{0}$ is not provable either. This is discussed in §3.4.

Answer 2

Just because something is unprovable doesn't mean it is false. For example, if $\phi$ is unprovable it means there exists both a model of your theory validating $\phi$ and one that validates $\neg\phi$. In particular this means you could add either as an axiom and your theory will be consistent (for example commutativity in group theory).

Now as already pointed out, your statement is indeed provable using univalence, but not for propositions.