The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Jan 17, 2014, at 2:06 PM, 
<drg AT illinois.edu>
 
<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) := ... .
> 

The effect in question is a corollary of a too aggressive use of implicit 
parameters. The parameter G can not be made implicit in this definition if 
one follows strict rules that the implicit parameters should be uniquely 
determined by the explicit ones.

In this case only (pr1 G) can be recovered from g and h but not G itself.

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

What does it mean? What would be the definition?

V.