Arithmetic in CC cats, query

Arithmetic in CC cats, query

[Colin McLarty]

	Take cartesian closed categories in the sense: having products, and
internal homs. If there is a natural number object you can define addition
NxN-->N with the usual recursion

		0+n = n          sm+n = s(n+m)

But can you prove it is commutative? You can prove 0+n=n+0 because you can
prove both = n. And you can prove each case of commutativity for "standard
natural numbers" in the sense of global elements sss..ss0 gotten from 0 by
(externally) finitely many applications of successor. 

	But even if I also assume equalizers, I do not see how to prove
commutativity for arbitrary global elements, let alone all generalized
elements. I suspect there are counterexamples but I cannot give one.

	I wonder if this is in Lambek and Scott, but my copy is at the office and
I will not be there until Monday so I am writing in to ask.

best, Colin