
> 
> **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](http://en.wikipedia.org/wiki/Integer#Construction). I am also aware of the nice [axiomatic characterization](https://mathoverflow.net/questions/23193/axiomatic-definition-of-integers) 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?



Direct construction of the integers
Informally speaking, taking the limit of [two's complement](http://en.wikipedia.org/wiki/Two%27s_complement) as the
number of bits goes to $\infty$,
the integers are just the eventually constant binary sequences (which
are naturally represented by finite binary sequences). 
For this to work, said sequences must start with the 
least significant bit, *i.e.,*
$1001011\overline{0}$ is interpreted as $2^0+2^3+2^5+2^6$ and
$1001010\overline{1}$ is interpreted as $2^0+2^3+2^5-2^7$.
The arithmetic and ordering of these strings is natural
(and efficient for microprocessors when we restrict
from $\mathbb{Z}$ to, say, $\{-2^{63},\ldots,2^{63}-1\}$).


The above can be reinterpreted as the following less direct construction. 
If $R$ is the inverse limit of rings
$\lim\_{\infty\leftarrow n}\mathbb{Z}/2^n\mathbb{Z}$, then the diagonal map 
$\Delta\colon\mathbb{Z}\rightarrow R$ given by 
$m\mapsto \lim\_{\infty\leftarrow n}(m\mod 2^n)$
is an injective ring homomorphism. [Edit: The image is characterized as the set of $\vec x\in R$ for which the truth value of $x(n+1)=x(n)$ is eventually constant.] Moreover, the ordering of $\mathbb{Z}$ is coded
via $m\geq 0\Leftrightarrow(m\mod 2^n: n\in\mathbb{N})$ is eventually constant.


**Update:** I couldn't resist the temptation to write a [functional programming implementation](http://codepad.org/BfuzCK5B).


