Univalent Foundations of Mathematics

 
Lectures
 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
8. Talk at IAS
    A type system with two kinds of 
    identity types, Feb. 25, 2013
    HTS_slides.pdf
Talk at ASL meeting 
    Univalent Foundations and Set Theory
    May 8, 2013.
  2013_ASL.pdf
  demo.v
 Lecture at IAS.
      Univalent Foundations
      March 26, 2014.
      2014_IAS.pdf
      
   
      Univalent_Foundations_files/2011_UPenn.pdfUnivalent_Foundations_files/demo.vUnivalent_Foundations_files/2011_Bergen.pdfUnivalent_Foundations_files/2011_Goteborg.pdfUnivalent_Foundations_files/2011_WoLLIC.pdfUnivalent_Foundations_files/demo_1.vhttp://video.ias.edu/univalent/voevodskyUnivalent_Foundations_files/Bonn_talk.pdfUnivalent_Foundations_files/Bonn_talk_coq.pdfUnivalent_Foundations_files/CMU_talk.pdfUnivalent_Foundations_files/HTS_slides.pdfUnivalent_Foundations_files/2013_ASL.pdfUnivalent_Foundations_files/demo_2.vUnivalent_Foundations_files/2014_IAS.pdffile://localhost/2013_ASL-6.pdfshapeimage_2_link_0shapeimage_2_link_1shapeimage_2_link_2shapeimage_2_link_3shapeimage_2_link_4shapeimage_2_link_5shapeimage_2_link_6shapeimage_2_link_7shapeimage_2_link_8shapeimage_2_link_9shapeimage_2_link_10shapeimage_2_link_11shapeimage_2_link_12shapeimage_2_link_13

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

Texts

  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)