Re: [HoTT] Re: Vladimir Voevodsky

[Michael Shulman <shu...@sandiego.edu>]

I met Voevodsky in 2010, when I was a postdoc at the University of
Chicago, and Steve Awodey invited me to CMU to hear Voevodsky talk
about his work on h-levels and univalence.  At the time I was still
struggling to wrap my head around type theory.  Voevodsky showed us
his Coq development, which ended with the construction of a function
assigning to each finite set its cardinality, and showing that Coq
could evaluate this function on the proof that finite sets are closed
under coproducts to compute something like 2+2=4.

Coming from homotopy theory and higher category theory, I found it
very natural to identify propositions with (-1)-types, and of course
every finite set should have a cardinality!  Finally, type theory
started to make sense to me.  This was the genius of his definitions
of h-level and univalence, which like many transformative innovations
seem inevitable in hindsight: they were the foundation stones of a
real bridge between type theory and higher category theory.