Homotopy Type Theory: Univalent Foundations of Mathematics

Homotopy type theory is a branch of mathematics that combines elements of homotopy theory and type theory to form a new foundation for mathematics called univalent foundations. It includes topics such as homotopy groups of spheres, algorithms for type checking, and the definition of weak ∞-groupoids. The univalence axiom and higher inductive types play a central role in this new foundation. The book is an introduction to the basics of univalent foundations and provides examples of this new style of reasoning without requiring any formal logic or computer proof assistance. The goal is for univalent foundations to eventually become an alternative to set theory as the foundation for informal mathematics.