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