Cartesian closed categories with double negation elimination

Question

Let $\mathcal{C}$ be a cartesian closed category with an initial object. The following facts are well known:

1. The initial object of $\mathcal{C}$ is strict: any morphism $X \to 0$ is necessarily an isomorphism.

2. The exponential object $0^{0^X}$ is subterminal: there is at most one morphism $T \to 0^{0^X}$ for any $T$.

3. There is a natural morphism $\eta_X : X \to 0^{0^X}$, namely $x \mapsto (f \mapsto f (x))$.

Question. According to a comment here, any natural morphism $c_X : 0^{0^X} \to X$ is necessarily a two-sided inverse of $\eta_X$. Why is this?

It is easy to see that $\eta_X \circ c_X$ is indeed the identity – this is a corollary of (2) above – but I have so far not been able to see why $\alpha_X \circ c_X$ is also the identity. Another easy observation is that the coproduct $1 \amalg 1$ is not disjoint; but this is hardly surprising, since $1 \amalg 1 = 1$ if $\mathcal{C}$ is a boolean algebra.

Also, how do we reconcile this with the idea that call-cc is a natural "morphism" of type $0^{0^X} \to X$?

Answer 1

By 1) $X \times 0 \approx 0$, so: $$\hom(X, 0^0) \approx \hom(X \times 0, 0) \approx \hom(0, 0) \approx \{\bullet\} \approx \hom(X, 1)$$ then by Yoneda $1 \approx 0^0 \approx 0^{0^1}$. Moreover $$\hom(0^{0^1}, 0^{0^X}) \approx \hom(1 \times 0^X, 0) \approx \hom(0^X, 0) \leq 1$$ Let us assume there is a natural transformation $\eta_X \colon 0^{0^X} \rightarrow X$ and there are two different global sections $a, b \colon 1 \rightarrow X$. Because $\eta_1$ is an isomorphism $a \not= b \Leftrightarrow a \circ \eta_1 \not= b \circ \eta_1$. By naturality of $\eta$ we have $\eta_X \circ 0^{0^a} \not= \eta_X \circ 0^{0^a}$, thus $0^{0^a} \not= 0^{0^b} \colon 0^{0^1} \rightarrow 0^{0^X}$, what leads to the contradiction since $\hom(0^{0^1}, 0^{0^X}) \leq 1$.

Therefore $\hom(1, X) \leq 1$ for any $X$. And, particularly, $\hom(A, B) \approx \hom(1, B^A) \leq 1$.

As for your second question, "call/cc" is not interpreted as a natural morphism in the naive way (notice that in the usual correspondence between classical calculus and lambda calculus, "terms" are enriched with control operators). You should enjoy reading a paper by Peter Selinger: "Control Categories and Duality".