Mehran Baghi

2. Introduction

“Tell readers that Introduction is not essential for book understanding”¹

The introduction gives a bird’s-eye overview of Homotopy type theory and its relation to other fields of mathematics. Unfortunately it intimidates newcomers and they might think that they won’t be able to understand the rest of the book. The good news is that the book is almost self sufficient. Although there is one subject that needs more explanation and that is Category theory. As one of the authors says:

“I think we did a fairly good job of not assuming too much background in topology and in type theory, but we did use a fair number of category-theoretic concepts without really explaining them in much detail”²

So it is a good idea to have an introduction to category theory. I don’t know much about category theory either, so if you do, and you want to contribute, please let us know by opening an issue on our GitLab.

With that being said, there is a great introductory video series on category theory by Steve Awodey on youtube: Category Theory Foundations, Lecture 1