I was playing around trying to formalize certain arithmetic properties using just the recursion theorem for a natural numbers object (as axiom) and using only universal properties and commutative diagrams.

I managed to formalize the sum and the product of natural numbers correctly.

But now I wanted to say that every natural number can be either odd or even, and I thought the best way to say this was that `N` is isomorphic to `2N ⨆ 2N+1`, for `⨆` the coproduct.

Now this might not be the best way to say that any natural number can be either odd or even, but my problem is even more basic. I don't know how to say what `2N` or `2N+1` are.

I know we can take the functor that makes the following square commute:

N -> N

| |

2^N -> 2^N

where the arrow from above is "multiply by 2" (to take `2N` as example); and now we can consider the map `1 -> 2^N` that chooses `N` from `2^N` which sent through the morphism from below in the square should be sent to `2N`, but it's such a messy definition, I can't really work with this, nor do I know how to write it down and use it in another diagram.

Any help?

Maybe it's just that I'm not seeing how to interpret correctly the "every natural number is either odd or even" proposition.

(Oh and by the way, I was trying to explicitely shy away from the Curry-Howard interpretation.)