Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
BTW: it's better to state such properties of F2 as functorial
registrations rather than theorems - this way they could be used
automatically by the checker when one would import your registrations.
I see your point, and when I was looking in the MML for examples on
which I could base my definition of F2, I found that functorial
registrations were the customary way of accomplishing my task.
Although I don't want to break with the custom and I understand the
value for the checker if I follow it, I do think that it is more
natural to express the properties of a new term as theorems rather
than as functorial registrations. By expressing properties in terms
of functorial registrations, one is writing for the MIZAR checker, not
for human readers. It seems to me that using functorial registrations
takes MIZAR away from rather than toward the mathematical vernacular.
(Though perhaps one could argue that the MIZAR custom of functorial
registrations is actually captures what's going on in the mathematical
vernacular.)