Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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$?

share|improve this question

1 Answer 1

up vote 2 down vote accepted

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".

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.