You are hereHome
Homotopy Type Theory
Univalent Foundations of Mathematics
The Univalent Foundations Program
Institute for Advanced Study
© 2013 The Univalent Foundations Program
MSC 2010 classification: 03-02, 55-02, 03B15
This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License.
This book is freely available at http://homotopytypetheory.org/book/.
Apart from the generous support from the Institute for Advanced Study, some contributors to the book were partially or fully supported by the following agencies and grants:
Association of Members of the Institute for Advanced Study: a grant to the Institute for Advanced Study
Air Force Office of Scientific Research: FA9550-11-1-0143, and FA9550-12-1-0370.
This material is based in part upon work supported by the AFOSR under the above awards. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author(s) and do not necessarily reflect the views of the AFOSR.
European Union’s 7th Framework Programme under grant agreement nr. 243847 (ForMath).
This material is based in part upon work supported by the National Science Foundation under the above awards. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
The Simonyi Fund: a grant to the Institute for Advanced Study
|Preface||PMBookProject||User not logged in|
|Introduction||PMBookProject||User not logged in|
|Part I Foundations||PMBookProject||User not logged in|
|Part II Mathematics||PMBookProject||User not logged in|
|HoTT Appendix A||PMBookProject||User not logged in|
- Planetary Bugs
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)
- Other useful stuff
new correction: examples and OEIS sequences by fizzie
new correction: Define Galois correspondence by porton
new correction: Closure properties on languages: DCFL not closed under reversal by babou
new correction: DCFLs are not closed under reversal by petey
new question: Lorenz system by David Bankom
new correction: Many corrections by Smarandache
new question: how to contest an entry? by zorba
new question: simple question by parag
new question: Latent variable by adam_reith