[2212.11082] Introduction to Homotopy Type Theory
source link: https://arxiv.org/abs/2212.11082
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
[Submitted on 21 Dec 2022]
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.
| Subjects: | Logic (math.LO); Category Theory (math.CT) |
| MSC classes: | 03B38 |
| Cite as: | arXiv:2212.11082 [math.LO] |
| (or arXiv:2212.11082v1 [math.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2212.11082 |
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK