The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

> set_of_suprema S == set_of_suprema T

Guessing what set_of_suprema would be, the above line does not mean "S
and T have the same supremum" but rather "if one of S or T has a
supremum then so does the other, and in this case the suprema are
equal".

> Or we can use Option from Coq core modules to represent a supremum or None 
> to mean no suprema.

That would work with classical logic but not in general. In general
you would have to define partial maps, like so (assuming my previous
file poset.v):

Definition subsingletons X := {p : X -> Prop | forall x y, p x -> p y -> x = 
y}.

Definition partial_map X Y := X -> subsingletons Y.

Definition sup {P : Poset} : partial_map (P -> Prop) P.
Proof.
  intro S.
  exists (supremum S).
  intros x y [H1 H2] [G1 G2].
  unfold upper_bound in * |- *.
  apply poset_asym; auto.
Defined.

And now you can write your "supremum S == supremum T" if you wish:

Definition same_supremum {P : Poset} (S T : P -> Prop) := (sup S = sup T).

But this is going to be less useful than using the relation "supremum S x".

With kind regards,

Andrej