The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

On Sun, Feb 22, 2009 at 6:50 PM, Samuel E. Moelius III
<moelius AT cis.udel.edu>
 wrote:
> Stéphane Lescuyer wrote:
>>
>> I'm not the author of this library but it seems to me that the carrier
>> is required in the definition of the partial order because it must be
>> non-empty.
>
> 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.

> Now that you mention it, though, it seems a bit odd to me to require a
> partial order to be non-empty.  But that is also probably a matter of taste.
>  :)
Now that you mention it, it seems a bit odd to me as well :) Plus I
can't find where this condition is used.

Stéphane L.
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06