The Coq mailing list

[Victor Porton <porton AT narod.ru>]

04.11.2011, 01:56, "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.

set_of_suprema S == set_of_suprema T

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

-- 
Victor Porton - http://portonvictor.org