Propositional truncation $||$-$||$ and double negation $\neg\neg$

Question

I have a basic question about propositional truncation $||$-$||$ and double negation $\neg\neg$.

According to the recursion rule of $||$-$||$, $A\rightarrow B=||A||\rightarrow B$ as long as $B$ is a mere proposition (i.e., proof-irrelevant). Now let $B=\neg\neg A$, since $\neg\neg A$ is a mere proposition, and $A\rightarrow\neg\neg A$ is a tautology, we naturally conclude that

$$||A||\rightarrow\neg\neg A.\quad\quad(1)$$

Since $||A||\rightarrow\neg\neg A$ is a tautology, then $\neg\neg(||A||\rightarrow\neg\neg A)$ is also a tautology. Since $\neg\neg$ distributes over $\rightarrow$, we get the following

$$\neg\neg||A||\rightarrow\neg\neg A.\quad\quad(2)$$

Therefore, the following is also true:

$$\neg\neg(||A||\rightarrow A).\quad\quad(3)$$

But (3) looks quite crazy because it's almost the inverse of $A\rightarrow||A||$, though under $\neg\neg$. I don't know if these are all correct. I would appreciate if someone can tell if it's correct or if there is anything wrong with my derivations.

---

More: Since there is a mapping for $A\rightarrow||A||$, its double negation $\neg\neg(A\rightarrow||A||)$ is also a tautology. Together with (3), we have $\neg\neg(A\leftrightarrow||A||)$. Is there any place wrong with my derivation?

Answer 1

Everything you’ve said works, and there’s a simple intuition for it all: $\neg\neg\cdot$ is a modality, and so is $\Vert\cdot\Vert$, and the latter is a “loosening” of the former. Specifically, they’re equivalent under the former (that is, $\prod_{A : \mathcal{U}} \neg\neg (\Vert A\Vert \simeq \neg\neg A)$), because we can prove $\mathrm{LEM}_{\neg\neg} :\equiv \prod_{A : \mathcal{U}} \neg\neg (A + \neg A)$. So if we assume $\mathrm{LEM}_{-1} :\equiv \prod_{A : \mathcal{U}} \mathrm{isProp}(A) \to \left\Vert A + \neg A\right\Vert$, then the two modalities are purely equivalent too.

The way I like to think about this is that, in a classical setting, propositional truncation is just the same thing as double negation, which is already well known to produce a classical environment in an otherwise constructive setting. So in the general constructive-by-default setting of MLTT and its descendants, propositional truncation isn’t automatically equivalent to double negation, but you also can’t prove that it’s disequivalent without an explicit anticlassicality principle—and they’ll always be equivalent in the “forced classical” environment underneath double negation.

Answer 2

Your arguments are correct as stated. It is indeed the case that the ($\Pi$-closures of the) types $\neg\neg (||A|| \rightarrow A)$ and $\neg\neg (||A|| \leftrightarrow A)$ are inhabited, and for the reasons outlined above.

The second part of your question far subtler: it asks about the "craziness" of the fact that these types are inhabited. I'm not sure how to answer this (although I suspect that a good answer is possible, and will eventually be penned by someone else). In the meantime, I offer a few remarks.

It's not surprising that we have functions $|| \bot || \rightarrow \bot$ or $||\mathbb{N}|| \rightarrow \mathbb{N}$ for fixed types $\bot, \mathbb{N}$. However, we certainly would not expect any term to inhabit $\Pi A:\mathbf{U}.||A|| \rightarrow A$. However, actually proving that there is no term of that type seems like a task that would involve fairly elaborate semantic reasoning (assuming that this is indeed the case; I might ask a followup question about this later).

The fact that we can construct an inhabitant of the type $\Pi A:\mathbf{U}.\neg\neg (||A|| \rightarrow A)$ is a pleasant surprise, but it does not say much about the inhabitedness of the former, as we still can't prove $\neg\neg \Pi A:\mathbf{U}.(||A|| \rightarrow A)$. In fact, there is a fairly direct proof of $\Pi A:\mathbf{U}.\neg\neg(||A|| \rightarrow A)$ that does not invoke the distributivity of $\neg\neg$, and might illuminate what's going on.

We can prove $\Pi A:\mathbf{U}.\neg(||A|| \rightarrow A) \rightarrow \neg A$ simply by taking $f : \neg(||A|| \rightarrow A)$ and $a : A$, and constructing $f(\lambda x.a) : \bot$. Similarly, we can prove $\Pi A:\mathbf{U}. \neg A \rightarrow ||A|| \rightarrow A$ since given $a : || A ||$ and $f: A \rightarrow \bot$ we can get $\mathrm{squashrec}(f): || A || \rightarrow \bot$, and then $\mathrm{squashrec}(f)(a) : \bot$. Putting these together we have a term of type $\Pi A:\mathbf{U}.\neg(||A|| \rightarrow A) \rightarrow || A || \rightarrow A$, from which $\Pi A:\mathbf{U}.\neg\neg(||A|| \rightarrow A)$ readily follows.