On Fri, 16 Nov 2007 09:23:28 +0100, Andrej Bauer wrote:
> 
> This construction is natural in the technical sense that it is left
> adjoint to the forgetful functor(*) from rings to rigs.

OK.

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

I do not think there is something natural about this construction in
the way you outlined it above.  It's just ad hoc for this case.

> The universal property of the resulting ring R is this: for any ring
> T, if f : M -> T is a function preserving 0, + and * then there is a
> unique function g : R -> T preserving 0, +, * and - such that g
> (include x) = f x, where include is as above. This needs to be
> accounted for, and it's not just a logical specification.

Would this fit your bill?

module type To_Ring = functor (M: RIG) -> sig
  include RING
  val embed : M.t -> t 
  module F : functor (T:RING) -> sig
    val lift : (M.t -> T.t) -> (t -> T.t)
  end
end

Regards,
ChriS