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?

constructed, but rahter thanwhat they are. Your proofs should not rely on any particular construction of the integers. That's my opinion. – Andrej Bauer Nov 8 '11 at 10:49