Re: [mizar] Re: Urelements?

[trybulec@math.uwb.edu.pl]

Cytowanie Josef Urban <josef.urban@gmail.com>:

> 2012/3/14  <trybulec@math.uwb.edu.pl>:
> > Cytowanie Josef Urban <josef.urban@gmail.com>:
> >
> >
> >
> > It does not matter that it is a new mechanism. It still does not work.
> >
> > Let be more precise: what yopu want to do with membership:
> >
> >
> >         let x,X be set;
> >         pred x in X;
> >
> > The membership takes structural arguments, so what Mizar is supposed to do?
>
> No, there is no structural argument in that definition.

So, by "takes a structural argument" you mean that the type of locus is
structural, do you? But then, if we write

     G in X
(G - a group) it would be coerced to

     the carrier of G in X,

But if G is a family of groups, and we write

          G in X
we mean exactly what it means without any coercion.

x = y

is not coerced at all, G1 = G2 means that the group are equal

x c= y

both arguments are coreced, G1 c= G2 means     the carrier of G1 c= the
carrier of G2

For the membership only the second argument is coerced. There are still
some minor problems e.g. how to cope with the redefinition of the
equality for sets

    redefine pred A = B means A c= B & B c= A

Regards,
Andrzej