Univalent Foundations Program.
Homotopy Type Theory: univalent foundations of mathematics.
Univalent Foundations Program. 2013
This book is freely available at http://homotopytypetheory.org/book/