The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Dear Dan,

We collected some references on this at the Institute:
http://uf-ias-2012.wikispaces.com/Type+classes

Best,

Bas

On Fri, Jan 17, 2014 at 8:06 PM, <drg AT illinois.edu> wrote:

One way to implement the notion of group G (for example) would be as a record,
the first element of which is the type X of the elements of the group.  The
multiplication operation could be defined with something like

   Definition op {G:Group} (g:pr1 G) (h:pr1 G) := ... .

where pr1 is projection on the first component.  If pr1 is defined as a
coercion,
then it can be written more suggestively as

   Definition op {G:Group} (g:G) (h:G) := ... .

If G' is another group sharing X with G, but not the other data, and g : G and
g' : G', then " op g g' " will be well-typed, which is mathematically
surprising
and might lead the user astray.

Assuming this issue has already been encountered in the past, I wonder what
the best solution is.  I'm tempted to say that an element g of G should be
defined
to be a pair (G,x) with x:X, and the coercion would then be the one that sends
G
to the type of such pairs.  This would be mathematically pleasing, as elements
of groups would know to which group they belong, just as elements of a type
"know" to which type they belong.

The actual situation where this arose was with two objects of a category and
the type of isomorphisms between them.