Prove that $a^1 \cong a$

Question

In Robet Goldblatt's 'The Categorial Analysis Of Logic', in section '3.16 Exponentiation', there is an exercise to prove that $a^1 \cong a$, and I have spent a while trying to get the right idea - which I suspect must be almost trivial, but it still eludes me. I am considering the following diagram:

Here I combine the diagrams for products of objects with the one for exponentiation (in the middle - I hope I've got them right), and that is where I'm stuck. I have chosen $pr_a \colon a \times 1 \rightarrow a$, which gives me $\hat{pr}_a \colon a \rightarrow a^1$, but how do I go the other way, so that I have an isomorphism?

Edit:

I don't think this is a duplicate - Goldblatt's book comes to this before mentioning Yoneda, so it should be possible to work this out using only Goldblatt's definition of exponentiation etc. I suspect that Yoneda may have followed a similar reasoning to get to the lemma.

Answer 1

Using the following diagram (taken from Awodey's book)

and setting $B=1$, and noting that $A\times 1\cong A$, because they are both products, we see that what this diagram says is that $\epsilon: C^1\times 1\to C$ is a terminal object in the category $(\mathscr C\downarrow C)$. But $1_C:C\to C$ is also terminal in $(\mathscr C\downarrow C)$ so $C^1\times 1\cong C$. To finish, note that $C^1\times 1\cong C^1$.

Answer 2

The inverse of your map $\hat{pr}_a$ is the composite $a^1\to a^1\times 1\to a$, where the first map is the unique one which is the identity on the first factor, and the second map is evaluation. Note that the first map is itself the inverse of $pr_a$, as you will probably want to have already proven to tackle this result.