The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Your example is strange.  Up to proof irrelevance, the type [BSig] has 
exactly one inhabitant (which is [Build_B "kilometers"]), so the 
coercion must be the constant function returning that value.

Julio wrote:
> I'm not sure what the rest of the definition Definition ASig_to_BSig : 
> ASig -> BSig := ... should be.
>
> On Wed, Sep 9, 2009 at 1:32 PM, Luke Palmer <lrpalmer AT gmail.com 
> <mailto:lrpalmer AT gmail.com>> wrote:
>
>     On Wed, Sep 9, 2009 at 5:01 AM, Julio 
> <coquser AT googlemail.com
>     
> <mailto:coquser AT googlemail.com>>
>  wrote:
>     > Is sigma type coercion possible?
>     >
>     > Require Import String.
>     > Open Scope string_scope.
>     > Record A:Set := {total:nat}.
>     > Record B:Set := {name:string}.
>     >
>     > (*Sigma types.*)
>     > Definition ASig := {a:A | (total a) > 10}.
>     > Definition BSig := {b:B | (name b) = "kilometers"}.
>     > (*Syntax for Coercion ASig >-> BSig ?*)
>
>     The same as all other coercions.
>
>     Definition ASig_to_BSig : ASig -> BSig := ...
>     Coercion ASig_to_BSig : ASig >-> BSig.
>
>     Luke