On Sunday, May 26, 2019 at 12:00:21 PM UTC-5, Kevin Buzzard wrote:
... But looking at
the things he formalised, he was doing things like the p-adic numbers,
and lots and lots of category theory. I am surprised that he did not
attempt to formalise the basic theory of schemes.
UniMath was formed from Voevodsky's Foundations (see
) and some formalizations based on it by other people, starting with Benedikt
Ahrens and me, and continuing with many others. In particular, the
formalization of category theory began with Ahrens' formalization of the material in a joint
paper of his with Kapulkin and Shulman, see
, and has been continued by other people, not Voevodsky.
Voevodsky was probably too busy writing his papers on the semantics of the system to turn to
formalizing the basic theory of schemes. For a while he said he wasn't even interested in formalizing
his proof of the Milnor conjecture, because he was confident it was correct. Then later he said, in a talk,
that it would be important top find a constructive proof of the Milnor conjecture, and to formalize it,
pinpointing a particular argument due to Merkurjev and Suslin as being non-constructive, see the remark
under the entry at
I also remember, perhaps in early 2014, that he told me he was thinking of formalizing the definition of scheme
(or maybe variety) so he could talk about it at a forthcoming talk, but he never did that.
Eventually UniMath should have the theory of schemes in it.
By the way, to go back to your original question, I think there are no "pain points" in formalizing
traditional mathematics in UniMath. The pain and challenge seem only to come when generalizing traditional facts
about sets so they apply also to types that are not assumed to be sets. For an example of that,
see Peter Lumsdaine's proof of transfinite induction into a family of types at
or see our proof with Bezem and Buchholtz that the type of ℤ-torsors satisfies the induction principle into
a family of types that the circle satisfies, at