Christophe TROESTLER wrote:
> I believe Z is generally defined as a quotient of the disjoint union
> (borrowed as variants in programming languages) of N and N
> (identifying the two 0).  Of course you can also define it as a
> quotient of N×N by the smaller equivalent relation "~" s.t. (n,m) ~
> (n+1,m+1) and it is quite nice as addition is "inherited" from the one
> on N×N but I am not sure it is the way it is usually done.

As another mathematician, also prone to nitpicking, I beg to differ. It 
is more natural to define Z as a quotient of N x N, because this is just 
a special case of a general construction of a (commutative) ring out of 
a (commutative) rig.

A rig is a structure with 0, + and * but no subtraction.

A ring is a structure with 0, +, - and *.

(Of course you need to imagine suitable axioms for 0, +, * such as 
commutativity, associativity and distributivity, but I am not writing 
them down here.)

 From every rig M we can construct a ring R as a quotient (M x M)/~ of M 
x M where we define

   (a,b) ~ (c,d)  iff  a+d = b+c

Think of (a,b) as the "non-existent" difference a-b. This construction 
is natural in the technical sense that it is left adjoint to the 
forgetful functor(*) from rings to rigs. (In non-mathematician language: 
if we already have + and *, there is a _best_ way of getting - as well.)

Caveat: (*) the use of "functor" here was as in mathematics, not as in 
ocaml.

In what way is natural, or canonical, the construction of Z defined by 
sticking together two copies of N?

To add some value to this post, other than mathematical willy waving, 
let me pose a puzzle. Implement the above in Ocaml, i.e., start with:

module type RIG =
sig
   type t
   val zero : t
   val add : t -> t -> t
   val mul : t -> t -> t
end

module type RING =
sig
   include RIG
   val sub : t -> t -> t
end

The puzzle is this: write down the module type for the construction 
taking a rig and returning the free ring over it. It is _not_ just

module type ConstructRing = functor (M : RIG) -> RING

because that would allow _any_ ring whatsoever as the result. It has to 
be the ring that comes from M via above construction, so there has to be 
extra stuff, such as an embedding of M into the resulting R. But what else?

Andrej