Arithmetic query answer

Arithmetic query answer

[Colin McLarty]

	Todd Wilson answered my query by politely pointing out the obvious--
that the function g:N-->N^N with g(m) = (lambda n)(sn+m) is defined by the
same induction on NxN as the function g':N-->NxN with g'(m) = (lambda
m)(m+sn). Namely, g(0) = successor, and gs = sg. And so the function
h:N-->N^N with h(m) = (lambda n)(m+n) is defined by the same induction as
h'(m)=(lambda n)(n+m), namely h(0)= 1_N and hs=sh.

	I'm afraid I manufactured a difficulty by focussing on Cartesian Closed
categories as "less than toposes" rather than thinking of them in their own
terms--so the "Peano axiom" kind of proof I was looking for is unavailable,
but no problem.

Colin