Univalent Foundations of Mathematics

 Talk at UPenn.
    Univalent Foundations, Sep. 22, 2011.
    a. 2011_UPenn.pdf
   b. demo.v
 Talk at TYPES2011 
    Resizing Rules, Sep. 11, 2011.
 Talk in Goteborg 
    Univalent Foundations, Sep. 5, 2011.
 Talk at WoLLIC 
    Univalent Foundations, May 18, 2011.
    a. 2011_WoLLIC.pdf
    b. demo.v
Talk at IAS 
Univalent Foundations, Dec. 10, 2010.
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.
8. Talk at IAS
    A type system with two kinds of 
    identity types, Feb. 25, 2013
Talk at ASL meeting 
    Univalent Foundations and Set Theory
    May 8, 2013.
 Lecture at IAS.
      Univalent Foundations
      March 26, 2014.

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

Coq files (“foundations”)

  1. 1. HTML-version of the library

2. Link to the source files


  1. 1.univalent_foundations_project.pdf (a modified version of an NSF grant application, Oct. 1, 2010)

  2. 2.Notes on type systems (minor update on Dec.13, 2011)expressions_current.pdf

  3. 3.A very short note on homotopy lambda calculus (Oct. 2, 2006).

  4. 4.homotopy_lambda_calculus_3.pdf (Jan.-Mar. 2006)