The equivalence axiom and univalent models of type theory. (Talk at CMU   on February 4, 2010)
  This is the text of my talk at CMU on Feb. 4, 2010 were I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). The first presentation of the axiom was in a lecture at LMU Munich in November 2009. 
Vladimir Voevodsky
math.LO