I am currently reading the HoTT book and came across exercise 3.14:
Show that assuming $\mathrm{LEM}$, the double negation $\neg \neg A$ has the same universal property as the propositional truncation $\| A \|$, and is therefore equivalent to it. Thus, under $\mathrm{LEM}$, the propositional truncation can be defined rather than taken as a separate type former.
The rules governing the truncation are:
Formation
- For every type A, $\|A\|$ is a type
Introduction
- For any $a:A$ we have $ |a| : \| A \|$.
- For any $x,y:\| A\|$, we have $x=y$.
Elimination resp. Recursion
- If $B$ is a mere proposition and we have $f:A\to B$, then there is an induced $g:\| A\| \to B$ such that $g(|a|) \equiv f(a)$ for all $a:A$.
My Problem
To proof the recursion principle for $\neg \neg A$ we first fix some $f:A\to B$ and then need to define $g:\neg\neg A\to B$. I don't know how to do that.
There are ways to use $\mathrm{lem:LEM}$, but I have no idea how to convert this terms (to assert judgemental equality), as $\mathrm{lem}$ is a primitive constant.
There is a solution in the Github folder HoTT/HoTT/contrib/HoTTBookExercises.v, that is programmed in Coq. Although I understood the argumentation I still don't see why it should be sufficient to proof $\neg\neg A \simeq \|A\|$ as we would end up with a propositional equality again.
I would really appreciate any help. Thanks in advance.
Best regards, Philipp
EDIT: I assume that $$\mathrm{LEM}=\mathrm{LEM}_{-1}=\prod_{A:\mathcal{U}}\mathrm{isprop}(A)\to A+\neg A. $$ just like the book does.
If what you're asking is whether $\neg\neg A$ has the same judgmental computation rule as $\Vert A \Vert$, then I think you're right that the answer is no.
To be precise, the exercise doesn't say to prove that $\neg\neg A$ has the same judgmental computation rule, or even the same induction principle, but the same universal property. The universal property of $\Vert A \Vert$ is unfortunately not stated in this section (it should be), but it appears as the $n=-1$ case of Lemma 7.3.3: for any mere proposition $B$, precomposition with $|-| : A \to \Vert A \Vert$ induces an equivalence
$$ (\Vert A\Vert \to B) \xrightarrow{\simeq} (A\to B).$$
This doesn't require a judgmental computation rule, and to say that $\neg \neg A$ has this same property is indeed the same as saying $\neg\neg A \simeq \Vert A \Vert$ (at least, assuming that $\Vert A \Vert$ exists).
However, it's clearly unreasonable to expect the reader to make this distinction for themselves, especially without having mentioned this universal property, and also especially because Exercise 3.15 does have the judgmental computation rule (at least for the recursion principle). I will submit a fix to the phrasing of the exercise, thanks for pointing this out.
For what it's worth, the judgmental computation rule of propositional equality is not very useful, because the target is always a mere proposition so that all its points are typally (i.e. "propositionally") equal anyway. The main thing I know of that you can do with the judgmental computation rule that you can't do without it is Kraus's magic trick, which might not be regarded as a good thing.