- Lecture at IHP, Paris. April 22, 2014.
Univalent Foundations - new type theoretic foundations of mathematics.
Note: this is a research talk not a systematic presentation of a subject.
- 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.
- Talk at ASL meeting
Univalent Foundations and Set Theory, May. 8, 2013.
- Talk at Andre Joyal's 70th birthday conference (IAS)
A type system with two kinds of identity types, Feb. 25, 2013
- Talk at UPenn
Univalent Foundations, Sep. 22, 2011.
- Talk at TYPES2011
Resizing Rules, Sep. 11, 2011.
- Talk in Goteborg
Univalent Foundations, Sep. 5, 2011.
- Talk at WoLLIC
Univalent Foundations, May. 18, 2011.
- Talk at IAS
Univalent Foundations, Dec. 10, 2010.
- Talk in Bonn
Univalent Foundations, Sep. 8, 2010.
- Talk at CMU
Univalent Model, Feb. 4, 2010.
Coq files ("foundations")
- HTML-version of the library
- Link to the source files
- Notes on type systems
Tuesday, December 13, 2011
- Univalent Foundations Project
(a modified version of an NSF grant application)
Friday, October 1, 2010
- A very short note on homotopy lambda calculus
Friday, October 2, 2009
- Notes on homotopy λ-calculus
Homotopy Lambda Calculus 3
Saturday, February 11, 2006