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

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