Univalent Foundations of Mathematics

About: Links on this page connect to different texts and videos related to the new foundations of mathematics which I am working on. Overviews can be found in “Talk in Goteborg” and in “Univalent foundations project”. There is also a link to the table of content of the current math library in Coq based on the Univalent Foundations which I am working on and to the source files of the library. A lot more can be now found at http://uf-ias-2012.wikispaces.com


  1. 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.
  2. Lecture at IAS, Princeton. Mar. 26, 2014.
    Univalent Foundations.
    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
  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.
  7. Talk in Goteborg
    Univalent Foundations, Sep. 5, 2011.
  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.
  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.

Coq files ("foundations")

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


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