Here's the problem:

Let $\mathbb{C}$ be a cartesian closed category with terminal object $1$. Show that $1^A\cong 1$ for all objects $A$ of $\mathbb{C}$.

This is said to be trivial and I'm not surprised. However, I'm stuck. I don't want to use the Yoneda Lemma since the notes I'm using haven't introduced it. They assume familiarity with $\lambda$-calculus, too, which is new to me; I get the impression that it's strongly related (thanks to the "Curry-Howard Isomorphism"). I'm entirely self-taught in Category Theory.

Definition: A cartesian closed category (CCC) is a category $\mathbb{C}$ with binary products, exponentials, and terminal objects; that is, the following functors have right adjoints: $$! :\mathbb{C}\to 1,$$ $$\Delta :\mathbb{C}\to\mathbb{C}^{\cdot\,\cdot},$$ and $$\_\times A:\mathbb{C}\to\mathbb{C}$$ for all objects $A$ of $\mathbb{C}$.

The following 'deduction' is allowed: $$\frac{1\times A\cong A, f: A\to B}{\bar{f}:1\to B^A},$$

where $\bar{f}$ is "internal" to $B^A$.

My attempt: Since $1$ is terminal, there exist unique $t_A: A\to 1$, $t_{1^A}: 1^A\to 1$. Clearly $$\frac{1\times A\cong A, t_A: A\to 1}{\bar{t_A}:1\to 1^A}$$ by the above deduction. We also have $\mathbb{C}(1\times A, 1)\cong\mathbb{C}(1, 1^A)$ since $\_\times A\dashv (\_ )^A$. But $\lvert\mathbb{C}(1\times A, 1)\rvert =1$ since $1\times A\cong A$ and $t_A$ is unique so $\lvert\mathbb{C}(1, 1^A)\rvert =1$ too.

I doubt that what I've done so far is right. It's probably way off. What I want to show now is that the compositions of $\bar{t_A}$ and $t_{1^A}$ are the identity morphisms.

Please help :)


Hint. To show that an object is isomorphic to the terminal $1$, it is not required to exhibit the isomorphism. Remember : the terminal object is defined by a universal property up to (unique) isomorphism.

Meaning that you can just show $1^A$ to satisfy this universal property. I let you take it from here.

  • $\begingroup$ Done it! Thank you, @Pece $\ddot\smile$ $\endgroup$ – Shaun Dec 7 '13 at 15:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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