Introduction to Homotopy Type Theory.
This is an introductory textbook to univalent mathematics and homotopy type
theory, a mathematical foundation that takes advantage of the structural nature
of mathematical definitions and constructions. It is common in mathematical
practice to consider equivalent objects to be the same, for example, to
identify isomorphic groups. In set theory it is not possible to make this
common practice formal. For example, there are as many distinct trivial groups
in set theory as there are distinct singleton sets. Type theory, on the other
hand, takes a more structural approach to the foundations of mathematics that
accommodates the univalence axiom. This, however, requires us to rethink what
it means for two objects to be equal. This textbook introduces the reader to
Martin-Löf’s dependent type theory, to the central concepts of univalent
mathematics, and shows the reader how to do mathematics from a univalent point
of view. Over 200 exercises are included to train the reader in type theoretic
reasoning. The book is entirely self-contained, and in particular no prior
familiarity with type theory or homotopy theory is assumed.
Read in full here:
This thread was posted by one of our members via one of our news source trackers.