[erik123]

Vladimir Voevodsky is making an interesting step when he says that rewrite steps in math are clearly homeomorphisms. I would like to see some more formal examples of that. It sounds like a promising path.

Concerning the replacement of ZFC by Russell types -- contrary to lambda calculus' functions -- I have not run often enough in illustrations that demonstrate the usefulness of Russell types.

I am personally much more vouching for a replacement of Zermelo and Fränkel's sets by Alonzo Church's functions than Bertrand Russell's types at this point. It is probably just an issue of lack of familiarity, though.