Question.Is there a direct construction of the integers which does not involve taking any quotients?

I am of course aware of the usual construction. I am also aware of the nice axiomatic characterization of the integers.

I am most interested in a **direct** construction. I am sure that one could probably use a disjoint union of $\mathbb{N}$ and $\mathbb{N}^{+}$ to construct $\mathbb{Z}$. But this involves 2 intermediate constructions (as well as dealing with cases).

**Edit.** By "direct construction", I mean something like the Peano construction for $\mathbb{N}$, seen as the inductive type built from $0$ and $\mathit{succ}$. Then one also constructs the operations of addition, multiplication, etc. Another way to think of it: suppose you wanted to have a datatype of "integers" in a lambda calculus which only allows inductive constructions and no quotients, how would you do it?

and forced us to do some workto get the integers? $\endgroup$17more comments