Univalent Foundations of Mathematics
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
Texts
1.univalent_foundations_project.pdf (a modified version of an NSF grant application, Oct. 1, 2010)
2.Notes on type systems (minor update on Dec.13, 2011)expressions_current.pdf
3.A very short note on homotopy lambda calculus (Oct. 2, 2006).
4.homotopy_lambda_calculus_3.pdf (Jan.-Mar. 2006)