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.
- UniMath
A lecture at the HLF 2016 that discusses Univalent Foundations including their developing nature and the UniMath library.
Slides
Video - Multiple concepts of equality in the new foundations of mathematics.
The opening lecture at FOMUS 2016, Bielefeld, July 18, 2016.
Slides - UniMath - a library of mathematics formalized in the univalent style.
A plenary lecture at the ICMS 2016 in Berlin, July 14, 2016.
Slides - 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 - UniMath
A short presentation at the Heidelberg Laureate Forum 2015
Slides - Univalent Morphisms.
A lecture at the NUS, Singapore, August 20, 2015.
Slides - From syntax to semantics of dependent types - formalized.
Plenary lecture at RDP, Warsaw, June 30, 2015.
Slides - C-systems - from monads and from universes in categories.
Lecture at the Department of Mathematics of Cornell, March 18, 2015.
Slides - Oxford lectures on UniMath filmed by Kohei Kishida
(only the last three out of six lectures were filmed)
Annotations
Lecture 4 (November 12, 2015) part1 part2
Lecture 5 (November 19, 2015) part1 part2
Lecture 6 (November 26, 2015) part1 part2 - Computer proof assistants and univalent foundations of mathematics.
Plenary talk at CMA2014, Kuwait. November 16, 2014.
Slides - 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. - Computer proof assistants - the future of mathematics.
Lecture at the NUS, Singapore. August 27, 2014.
Slides - How I became interested in foundations of mathematics.
Lecture at the 8th Asian Science Camp in Singapore. August 25, 2014.
Slides
Note: It was a lecture for undergraduates. Here is one of the posters that the listeners made after the lecture. - Dependently-typed systems and their models.
Lecture at a workshop in IHP, Paris. June 6, 2014.
Slides
Note: this is a very messy workshop talk. - Univalent Foundations - new type theoretic foundations of mathematics.
Lecture at IHP, Paris. April 22, 2014.
2014_04_22_slides.pdf
Video on YouTude
Note: this is a research talk not a systematic presentation of a subject. - Univalent Foundations.
Lecture at IAS, Princeton. Mar. 26, 2014.
2014_IAS.pdf
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. - Univalent Foundations of Mathematics
Heidelberg Laureates Forum, September 26, 2013.
Video - Univalent Foundations and Set Theory
Plenary lecture at ASL meeting, May 8, 2013.
a. 2013_ASL.pdf
b. demo.v - A type system with two kinds of identity types,
Talk at Andre Joyal's 70th birthday conference (IAS), Feb. 25, 2013
HTS_slides.pdf
HTS_notes.pdf
Note: This is the talk where the idea of HTS was introduced. - 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. - Resizing Rules
Plenary lecture at TYPES2011, Sep. 11, 2011.
2011_bergen.pdf
Note: this is the talk where the concept of resizing rules was introduced. - Univalent Foundations
Talk in Gotenborg, Sep. 5, 2011.
2011_goteborg.pdf
Warning: this talk contains false attributions of some ideas to S. Awodey. - Univalent Foundations of Mathematics
Talk a Templeton meeting, July 22, 2011.
Slides
Warning: this talk contains false attributions of some ideas to S. Awodey. - 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. - Univalent Foundations
Talk at IAS, Dec. 10, 2010.
video
Warning: this talk contains false attributions of some ideas to S. Awodey. - What if the current foundations of mathematics are inconsistent?
Lecture at the celebration of the 80s anniversary of the IAS. September, 25, 2010.
Slides
Video - 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. - Univalent Model
Talk at CMU, Feb. 4, 2010.
CMU_talk.pdf
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. - Foundations of Mathematics and Homotopy Theory
IAS faculty lecture, March 22, 2006
Video
Slides - Mathematics and the outside world
Plenary lecture at AMS-India meeting Bangalore, Dec. 17-20, 2003.
Transparencies - 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) - Intuitive introduction to the motivic homotopy theory
Clay Mathematical Institute annual meeting, October 2002.
Transparencies
Video - From motives to motivic homotopy types
Visions in Mathematics, Tel Aviv, August-September 1999
Transparencies - Motivic homotopy type?
Chicago, Fall 1998
Transparencies - Homotopy Theory of Algebraic Varieties
Plenary lecture at ICM1998, Berlin, August 21, 1998
Transparencies
