Lectures
 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.
 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.
 Talk at ASL meeting
Univalent Foundations and Set Theory, May. 8, 2013.
a. 2013_ASL.pdf
b. demo.v
 Talk at Andre Joyal's 70th birthday conference (IAS)
A type system with two kinds of identity types, Feb. 25, 2013 HTS_slides.pdf
 Talk at UPenn
Univalent Foundations, Sep. 22, 2011.
a. 2011_UPenn.pdf
b. demo.v
 Talk at TYPES2011
Resizing Rules, Sep. 11, 2011. 2011_bergen.pdf
 Talk in Goteborg
Univalent Foundations, Sep. 5, 2011. 2011_goteborg.pdf
 Talk at WoLLIC
Univalent Foundations, May. 18, 2011.
a. 2011_WoLLIC.pdf
b. demo.v
 Talk at IAS
Univalent Foundations, Dec. 10, 2010. video
 Talk in Bonn
Univalent Foundations, Sep. 8, 2010.
a. Bonn_talk.pdf
b. Bonn_talk_coq.pdf
 Talk at CMU
Univalent Model, Feb. 4, 2010. CMU_talk.pdf

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