[mizar] Why do Mizar types have to be non-empty?

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

Hello,

Can someone explain to me _why_ Mizar types have to be
non-empty?  It's very inconvenient!  Often there are things
that I would like to write as a type, but I cannot do so,
because that type might be non-empty.  (For instance, in
rewriting, one would like to have a type "Normal_form of t",
but some terms t don't have a normal form!)  I mean, if Mizar
doesn't exclude the empty set from its set theory, why does
it exclude empty types from its type theory?  Of course I'm
used to Coq in which non empty types are nothing special.

Also, if Mizar allowed empty types, one wouldn't need to
prove all those tiresome "existence" correctness conditions,
and there wouldn't need to be existential clusters.  So
what's the use of all that, except as a sanity check on the
definitions?  There is no _mathematical_ reason for them, is
there?

Also, I think that because of this, there are more "non
empty" adjectives in the MML than it would else be the case.

Freek