[FOM] New Umbrella?

[Freek Wiedijk]

Dear Urs,

>Moreove I still don't see any prospect of anyone writing
>non-trivial formal ZFC code.

Sorry, but maybe I'm missing something here.  If I formalize
in Mizar, then underneath there is "non-trivial formal ZFC
code".  And Josef Urban's PhD was about actually getting
that formal ZFC code out, in the standard format for FOL
proofs, the TPTP format.

So do you mean formalizing a HoTT model in Mizar would not
be doable?  Or are you just saying that you don't expect
anyone to actually _do_ that?  In the latter case you might
be right, HoTT is not _that_ interesting to people outside
of the HoTT community.

I don't know how much work it would be to formalize the
simplicial set model (or cubical set model) in Mizar.
Mizar has a formalization of category theory already (in
fact, there's more than one :-)), so that could be used.
How many pages is the definition of that model in English?

(And you never answered my question how many lines of
Agda code the proof of that Blakers-Massey thing was
if you counted all the definition/lemmas that it used
from earlier libraries with it?  I'm still very much
interested in that number!  Is it possible to extract that
"minimal" subformalization for a given lemma in Agda?
Automath had that feature at some point (in fact, my
Automath-reimplementation from the nineties has it too :-)))

Freek