Re: [mizar] weak types

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

On Wed, 19 Nov 2003, Andrzej Trybulec wrote:

> With a permissive definition like (NATTRA_1:def 8):
> 
>  let A,B be Category, F1,F2 be Functor of A,B;
>  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;

Just repeating the argument from previous post, this seems to me pretty 
unnatural :-). If we defined predicate 
"t is_natural_transformation_of F1,F2"  in the corresponding way, your
definition just says:

assume A1: ex t st t is_natural_transformation_of F1,F2;
mode natural_transformation of F1,F2 -> transformation of F1,F2 means
     it is_natural_transformation_of F1,F2; 
existence by A1;

> when one proves that a transformation is a natural transformation, then one
> has to prove first the guard (the assumption in the definition) 

So before I am allowed to prove, that t is natural, I have to prove that 
there is something natural. Thanks.

> and then the
> definiens, like in the proof of coherence in NATTRA_1:def 9

This would be much nicer as attribute "natural" defined for 
"transformation of F1,F2", and then as exactly the same kind of functor 
cluster as I described previously (but now for t2'*'t1), needing weak 
types in loci. 

> So the difference seems to be in the fact, that you want to state the guard,
> if you just write
>       T is natural_transformation
> and in Mizar we need guard only when the definition is actually used. It is
> something like lazy evaluation.
> I believe it is the main argument for the permissiveness.

The permissiveness might be good for functions like sqrt, I am not sure. 
But for types, the only "advantage" of permissive over weak is, that 
you can "consider" them even in cases when they "are empty", knowing 
exactly nothing in such cases. For weak types, if you find out that you 
are in the empty case, you can trivially prove anything right away, which 
(I repeat myself) is the common mathematical understanding.

Josef