The Coq mailing list

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

>> Dear Daniel,
>
> I'm Victor, not Daniel.

Oops, I apologize.

> I will restate my problem again.
>
> I want syntax similar to the following:
>
> "supremum S == a".

You can define a relation "is_supremum S a" and then define a special
Notation so that you can write "supremum S == a" if you really want
to. But I would advise against it. Not every informal syntax invented
by mathematicians makes sense.

> I want the following to come true:
>
> "a in X /\ S is a subset of X /\ supremum S = a -> S has a supremum"

This is a triviality because you would write it as (continuing from
the file I sent):

    Definition has_supremum {X : Poset} (S : X -> Prop) := exists x :
X, supremum S x.

    Theorem victor_or_daniel (X : Poset) (a : X) (S : X -> prop) :
supremum S a -> has_supremum S.
    (* proof left as exercise *)

> How to do it with type theory? I ZF I can define "y" in such a way that "y 
> not in S" and use "supremum S == y" to denote that S has no supremum. I see 
> no alternative for this in type theory except to formalize some universe of 
> sets (for example ZF) and work inside this universe. So to have this syntax 
> convenience ZF is essentially unavoidable (at least so it seems to me).

The alternative is to say simply

Definition has_no_supremum {X : Poset} (S : X -> Prop) := not exists x
: X, supremum S x.

Why do you want that y? Just so that you can use your informal
notation "supremum S == y" for two purposes, one of which makes little
sense? Just stop using the broken informal notation and life will be
easier.

With kind regards,

Andrej