Hi,

On Thu, 15 Nov 2007 14:26:49 +0100, Pierre Weis wrote:
> 
> we define Z (the set of relative integer numbers) as a quotient of NxN),

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.

>  In the previous definition of quotient structures, there is a
> careful distinction between the base set S and the quotient set
> S/R. In fact, there always exists a canonical injection from S to S/R,

Sorry for the nit-picking (I'm a mathematician, you know how we
are :) ), but unless R is diagonal, the function S -> S/R is not
injective (since we identify R-equivalent elements) but it is
surjective.

> We understand why the mathematicians always write after having designed a
> quotient structure: ``thanks to this isomorphism, and if no confusion may
> arise, we always assimilate S to its canonical injection in S/R''.

By the above remark, S can be identified to a subset of S'/R for some
S' but definitely not (of) S/R.

> (...)
> - the canonical projection from S/R to S is automatic.
> (...)
> More exactly, the canonical injection from S to S/R maps each element of S to
> its equivalent class in S/R; if we assimilate each equivalence class to its
> canonical representant (an element of S), the canonical injection maps each
> element of S to the canonical representant of its equivalence class. Hence
> the canonical injection has type S -> S.

This is rather the projection (and generally not an injection) as,
mathematically, p : S -> S is a projection means p(p x) = p x, forall x.
Moreover, in the abstract, there is no canonical representative of an
equivalent class -- that depends on the situation at hand.

Given your example (deleted), I suppose what you mean is that the
projection S -> S (representing S -> S/R) has to be written (since one
has to actually choose a representative) while the injection S/R -> S
comes for free or up to a coerecion (since we identified S/R to a
subset of S).

> What about private abbreviations ? (...)
> If not implicit, the injection function should granted to be the
> identity function (something that we would get for free, if we allow
> projection via sub-typing coercion).

I second the use of a subtyping coercion for that (after all, it would
be really annoying to have to use a private type abbreviation from a
module "forgetting" to provide a way out :) ).

> The moca compiler (see http://moca.inria.fr/) helps you to write the
> canonical injection by generating one for you, provided you can express the
> injection at hand via a set of predefined algebraic relations (and/or rewrite

May you tell a bit more ?  That looks quite interesting ! Since there
is nothing canonical about the injection S/R -> S, what does moca do
if several representatives are possible (e.g. pick one by preferring
left associativity to the right one?).  (I saw there is some paper on
the page but I have no time to dig through it right now.)

Best regards,
ChriS