The Coq mailing list

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

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.

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

Sam