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 

    https://github.com/UniMath/Foundations

) 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 

    
https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/README.md

, 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 

   
http://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#UniMath-1

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

    
https://github.com/UniMath/UniMath/blob/master/UniMath/Combinatorics/WellFoundedRelations.v#L208

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

    https://github.com/UniMath/SymmetryBook/blob/master/ZTors.tex

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d57bb2de-ff98-484b-8bc0-9c3f31620a47%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.