The Coq mailing list

["Daniel R. Grayson" <drg AT illinois.edu>]

On Sun, Jan 19, 2014 at 9:08 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

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.

Yes, that strict rule is a good idea, which I was violating.

 

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

Good question.  Given G : Group, we could define Elem G to be the type

of all pairs (H,x) where H is (definitionally) equal to G and x : pr1 H (if we had

"singleton types", which coq doesn't have).  Then a judgment g:Elem G

would uniquely determine G.

 

V.