The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

Stéphane Lescuyer wrote:
> <moelius AT cis.udel.edu>
>  wrote:
> > I would think that there would have to be other reasons as well.  For
> > example, this condition alone could be achieved with
> >
> > Record PO (U : Type) : Type := Definition_of_PO
> >    { Rel_of : Relation U;
> >      PO_cond1 : Inhabited U (fun _ : U => True);
> >      PO_cond2 : Order U Rel_of }.
> >
> > which I would think is simpler than having the ``Carrier_of'' field.
>
> This condition alone, indeed. But then you wouldn't have a way to talk
> about the carrier of the relation. U itself is not a carrier, it is a
> Type, and in this library, sets are encoded as Type -> Prop and the
> carrier should be a subset of U in that sense. The carrier is then
> used to define properties on partial orders, see Lubs, Lower Bounds
> etc in Coq.Sets.Cpo for instance.

Please let me rephrase my question then.  Consider the following two 
approaches.

(1) What is now done in the library (using the ``Carrier_of'' field).

(2) Doing something similar to what I wrote above, letting U be a 
sigma-type, if necessary.

What are the advantages of (1) over (2)?  Or is it just a matter of taste?

Stéphane: Thanks for your help, BTW.  :)

Sam