Re: [mizar] Once more: empty types

[Freek Wiedijk <freek@cs.ru.nl>]

Hi Piotr,

>I have trouble imagining  the consequences of allowing
>Mizar types to be possibly empty.

Well, one of the consequence would be that no one will
prove the existential clusters anymore that really they
should prove...

>Before this happens, my lack of experience with p.e. types
>makes me look at them as not 'natural'.

I'm sure that my experience with them in type theory is
what makes me look at them in the opposite way.  We're all
shaped by our experiences.

Freek