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