The Coq mailing list

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

>>>  But what if I want to write "supremum S == supremum T"? (to add more 
>>> complexity, the first and the second supremum may be taken on different 
>>> sets.)
>>
>> You could write for example as
>>
>>    exists x, supremum S x /\ supremum T x
>
> It is bad to introduce an extra variable.

You can still write "supremum S == supremum T" if you mutliate Coq's
notation mechanisms enough. But as I said, don't go crazy with
misleading notation.

By the way, if supremum of S is computed in the poset P and supremum
of T is computed in the poset Q, then in type theory it does not make
sense to compare the suprema. More generally, if x has type X and y
has type Y, then it makes no sense to state or ask "x = y". It's
simply not something you can write down. You may think this is an
obstacle, but it isn't.

If you know how to express the fact that S and T have the same
supremum without using any quantifiers, please let me know.

With kind regards,

Andrej