Return to Question

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?

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?

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?

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?

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}$.

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?