New (July 15, 2016) : Slides for the plenary ICMS 2016 lecture and the opening talk at FOMUS 2016 are added. 

New(Oct. 18, 2016) : Video from the HLF 2016 added.

  1. UniMath
    A lecture at the HLF 2016 that discusses Univalent Foundations including their developing nature and the UniMath library.
  2. Multiple concepts of equality in the new foundations of mathematics. 
    The opening lecture at FOMUS 2016, Bielefeld, July 18, 2016.
  3. UniMath - a library of mathematics formalized in the univalent style.
    A plenary lecture at the ICMS 2016 in Berlin, July 14, 2016.
  4. Dependent Type Theories
    Lectures in the Max Planck Institute in Bonn. February 10-14, 2016.
    Lecture 1. Slides.
    Lecture 2. Slides.
    Lecture 3. Slides.
    Lecture 4. Slides.
    Lecture 5. Slides
  5. UniMath
    A short presentation at the Heidelberg Laureate Forum 2015
  6. Univalent Morphisms.
    A lecture at the NUS, Singapore, August 20, 2015.
  7. From syntax to semantics of dependent types - formalized.
    Plenary lecture at RDP, Warsaw, June 30, 2015.
  8. C-systems - from monads and from universes in categories.
    Lecture at the Department of Mathematics of Cornell, March 18, 2015.
  9. Oxford lectures on UniMath filmed by Kohei Kishida 
    (only the last three out of six lectures were filmed)
    Lecture 4 (November 12, 2015) part1 part2
    Lecture 5 (November 19, 2015) part1 part2
    Lecture 6 (November 26, 2015) part1 part2
  10. Computer proof assistants and univalent foundations of mathematics.
    Plenary talk at CMA2014, Kuwait. November 16, 2014. 
  11. Foundations of mathematics - their past, present and future.
    The 2014 Paul Bernays Lectures at ETH Zurich. Sep. 9-10, 2014. 
    I. To the history of the conception. Slides Video
    II. The story of set theory (so far). Slides Video
    III. Univalent Foundations. Slides Video
    Note: there is a lot in the videos that is not in the slides. 
  12. Computer proof assistants - the future of mathematics.
    Lecture at the NUS, Singapore. August 27, 2014.
  13. How I became interested in foundations of mathematics. 
    Lecture at the 8th Asian Science Camp in Singapore. August 25, 2014.
    Note: It was a lecture for undergraduates. Here is one of the posters that the listeners made after the lecture. 
  14. Dependently-typed systems and their models.
    Lecture at a workshop in IHP, Paris. June 6, 2014. 
    Note: this is a very messy workshop talk. 
  15. Univalent Foundations - new type theoretic foundations of mathematics.
    Lecture at IHP, Paris. April 22, 2014.
    Video on YouTude
    Note: this is a research talk not a systematic presentation of a subject.
  16. Univalent Foundations.
    Lecture at IAS, Princeton. Mar. 26, 2014.
    Note: This is a general audience talk which is partly autobiographical
    with the discussion of the role of mistakes in mathematics. Here is an article that was made from it.
  17. Univalent Foundations of Mathematics
    Heidelberg Laureates Forum, September 26, 2013.
  18. Univalent Foundations and Set Theory
    Plenary lecture at ASL meeting, May 8, 2013.
    a. 2013_ASL.pdf
    b. demo.v
  19. A type system with two kinds of identity types,
    Talk at Andre Joyal's 70th birthday conference (IAS), Feb. 25, 2013
    Note: This is the talk where the idea of HTS was introduced.
  20. Univalent Foundations
    Talk at UPenn, Sep. 22, 2011.
    a. 2011_UPenn.pdf
    b. demo.v
    c. Video on YouTube.
    Warning: this talk contains false attributions of some ideas to S. Awodey. 
  21. Resizing Rules
    Plenary lecture at TYPES2011, Sep. 11, 2011.
    Note: this is the talk where the concept of resizing rules was introduced.
  22. Univalent Foundations
    Talk in Gotenborg, Sep. 5, 2011. 
    Warning: this talk contains false attributions of some ideas to S. Awodey.
  23. Univalent Foundations of Mathematics
    Talk a Templeton meeting, July 22, 2011.
    Warning: this talk contains false attributions of some ideas to S. Awodey.
  24. Univalent Foundations
    Plenary lecture at WoLLIC, May. 18, 2011.
    a. 2011_WoLLIC.pdf
    b. demo.v
    Warning: this talk contains false attributions of some ideas to S. Awodey.
  25. Univalent Foundations
    Talk at IAS, Dec. 10, 2010.
    Warning: this talk contains false attributions of some ideas to S. Awodey.
  26. What if the current foundations of mathematics are inconsistent?
    Lecture at the celebration of the 80s anniversary of the IAS. September, 25, 2010. 
  27. Univalent Foundations
    Talk in Bonn, Sep. 8, 2010.
    a. Bonn_talk.pdf
    b. Bonn_talk_coq.pdf
    Warning: this talk contains a mistaken attribution of some ideas to S. Awodey.
  28. Univalent Model
    Talk at CMU, Feb. 4, 2010.
    Video: part1 part2 part3 part4
    Note: this is the talk that was the starting point of the current stage of development of the univalent foundations.
  29. Foundations of Mathematics and Homotopy Theory
    IAS faculty lecture, March 22, 2006
  30. Mathematics and the outside world
    Plenary lecture at AMS-India meeting Bangalore, Dec. 17-20, 2003.
  31. Two lectures
    Wuhan University 110th anniversary, November-December 2003
    What is most important for mathematics in the near future? (Notes)
    About mathematics and motivic homotopy theory (Transparencies)
  32. Intuitive introduction to the motivic homotopy theory
    Clay Mathematical Institute annual meeting, October 2002.
  33. From motives to motivic homotopy types
    Visions in Mathematics, Tel Aviv, August-September 1999
  34. Motivic homotopy type?
    Chicago, Fall 1998
  35. Homotopy Theory of Algebraic Varieties
    Plenary lecture at ICM1998, Berlin, August 21, 1998