Vladimir Voevodsky

icon indicating a website link http://www.math.ias.edu/vladimir/

icon location Vladimir Voevodsky died September 30, 2017. This account is maintained in memoriam by Dan Grayson as his academic executor, http://dangrayson.com/.

Results 23 comments of Vladimir Voevodsky

Use and introduction of identity types

This requires k < n which requires universe. As soon as you have a universe there are very simple examples. V. > On Oct 20, 2014, at 9:38 PM, Andrej...

Use and introduction of identity types

T:U If we had El we would have written El(T). This is the most fundamental example of a dependent type together with the identity. V. > On Oct 21, 2014,...

How to insert new theorems in edition 1

There is some standard way which is used in libraries. I am away from the IAS at the moment so I can not check it out but it is probably...