Re: [mizar] weak types

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

> Removing the fictitious variables is a comparatively new feature, and I hope that
> we remove the removing.

Which one? :-)

> So, the quantifiers are ignored. If you have as a premise
>        for x being S, y be T holds P[x]
> you may infer P[a]. If T was empty, the sentence above would be true for any P[.].

So we would have to force the instantiation in such cases, either 
explicitly in the "Unifier", or by Freek's encoding as implication.
It almost seems to me that the result would be the same now. 

> It is basically the same as
> Freek's example. Is it a deeper reason?

Certainly lurking deep enough in the checker :-).

> The typical way to cope with the situation is to use permissiveness
> 
>  definition let G,H be Group such that
> A: G,H are_isomorphic;
>    mode Isomorphism of G,H means
>     .....;
>    existence by A;
>  end;

But that does not apply to clusters, and clusters are more 
frequent and usually preferable to modes (especially now, when the 
nonclusterable attributes are gone). It fixes the type hierarchy, but 
the price is that you have to drag along the assumptions, if you need the 
definiens. So you can end up with funny implications like:

ex M being Cardinal st M is_measurable implies
for N being MeasurableCardinal holds N is inaccessible. 

Josef