Hi Jesse,
This may be somewhat inappropriate for mizar-forum, but it seems noteworthy to me that in the non-exhaustive list of systems for dependent types mentioned in this recent post to the TYPES forum, mizar is not mentioned. Would it be appropriate to write an article on mizar's dependent types for the upcoming special issue of Fundamenta Informaticae? One initial question to consider: does mizar's type system differ in any interesting way from the type sytems mentioned below?
I think the reason why the Mizar type system is not mentioned is that people know very little about it. And it seems to me that there is practically no research being done on Mizar type system, even though it is a very "practical" and notrivial thing to have good "type" automation over set theory. And yes, Mizar's type system significantly differs from others. So I think it is a very good idea to do more research and publish about it.
Josef