Homotopy Type Theory Univalent Foundations of Mathematics

This book is the product of a yearlong collaboration at the Institute for Advanced Study. It describes (the beta version of) a new language for mathematics, which may some day replace set theory.