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?
Best Answer
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.