Lectures

1. Lecture at IHP, Paris. April 22, 2014.
   Univalent Foundations - new type theoretic foundations of mathematics.
   2014_04_22_slides.pdf
   Note: this is a research talk not a systematic presentation of a subject.
2. Lecture at IAS, Princeton. Mar. 26, 2014.
   Univalent Foundations.
   2014_IAS.pdf
   Note: This is a general audience talk which is partly autobiographical
   with the discussion of the role of mistakes in mathematics.
3. Talk at ASL meeting
   Univalent Foundations and Set Theory, May. 8, 2013.
   a. 2013_ASL.pdf
   b. demo.v
4. Talk at Andre Joyal's 70th birthday conference (IAS)
   A type system with two kinds of identity types, Feb. 25, 2013
   HTS_slides.pdf
5. Talk at UPenn
   Univalent Foundations, Sep. 22, 2011.
   a. 2011_UPenn.pdf
   b. demo.v
6. Talk at TYPES2011
   Resizing Rules, Sep. 11, 2011.
   2011_bergen.pdf
7. Talk in Goteborg
   Univalent Foundations, Sep. 5, 2011.
   2011_goteborg.pdf
8. Talk at WoLLIC
   Univalent Foundations, May. 18, 2011.
   a. 2011_WoLLIC.pdf
   b. demo.v
9. Talk at IAS
   Univalent Foundations, Dec. 10, 2010.
   video
10. Talk in Bonn
    Univalent Foundations, Sep. 8, 2010.
    a. Bonn_talk.pdf
    b. Bonn_talk_coq.pdf
11. Talk at CMU
    Univalent Model, Feb. 4, 2010.
    CMU_talk.pdf

Coq files ("foundations")

1. HTML-version of the library
2. Link to the source files

Texts

1. Notes on type systems
   (minor update)
   Tuesday, December 13, 2011
   expressions_current.pdf
2. Univalent Foundations Project
   (a modified version of an NSF grant application)
   Friday, October 1, 2010
   univalent_foundations_project.pdf
3. A very short note on homotopy lambda calculus
   Friday, October 2, 2009
   Hlambda_short_current.pdf
4. Notes on homotopy λ-calculus
   Homotopy Lambda Calculus 3
   Saturday, February 11, 2006
   homotopy_lambda_calculus_3.pdf