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

[Andrzej Trybulec <trybulec@cs.shinshu-u.ac.jp>]

Freek Wiedijk wrote:

> >BTW. Are you sure that your 'normal form' is a type, not an attribute?
>
> I guess "normal" is an attribute, while "normal form" is a
> type.  It's like "natural number": "natural" is an attribute,
> but "natural number" is a type.
>

Right, I was sloppy. But what you really define is an attribute and the
"Normal_form" is expandable mode. Am I right?


>
> I want to be able to say "reserve n for Normal_form of R;"
> (where "R" is some kind of reduction relation") and then
> later "consider n such that ..."
>

You may use a permissive definition, say

definition let R be redunction-relation such that
Z:  R has_normal_forms;
  mode Normal_form of R means
   it is_normal_form;
  existence by Z;
end;


> See <http://www.cs.kun.nl/~freek/notes/newman.ps.gz> for a
> proof where this seemed the most natural way to do things.
> (In that particular example I gave "R" the attribute
> "nf_inhabited", just to get around this.)

That's OK. But then you cannot use it for an arbitrary reduction relation.I
it hard to decide, in many cases, which solution is better. I used the
similar approach, that I proposed above, then I got something like
NATTRA_1:def 3, def 8:

 reserve A,B for Category,  F1,F2 for Functor of A,B;

 let A,B,F1,F2;
 assume  F1 is_transformable_to F2;
 mode transformation of F1,F2 -> Function of the Objects of A, the
Morphisms of B means
 for a being Object of A holds it.a is Morphism of F1.a,F2.a;

and

let A,B,F1,F2;
 assume F1 is_naturally_transformable_to F2;
 mode natural_transformation of F1,F2 -> transformation of F1,F2 means
   for a,b being Object of A st Hom(a,b) <> {}
   for f being Morphism of a,b holds it.b*F1.f = F2.f*it.a;

A bit boring, introducing and working with these predicates, but I got a
quite flexible language.

Regards,
Andrzej