A Primer on Homotopy Type Theory Part 1: The Formal Type Theory

This Primer is an introduction to Homotopy Type Theory (HoTT). The original source for the ideas presented here is the ``HoTT Book'' -- Homotopy Type Theory: Univalent Foundations of Mathematics published by The Univalent Foundations Program, Institute for Advanced Study, Princeton. In what follows we freely borrow and adapt definitions, arguments and proofs from the HoTT Book throughout without always giving a specific citation. However, whereas that book provides an introduction to the subject that rapidly involves the reader in advanced technical material, the exposition in this Primer is more gently paced for the beginner. We also do more to motivate, justify, and explain some aspects of the theory in greater detail, and we address foundational and philosophical issues that the HoTT Book does not. In the course of studying HoTT we developed our own approach to interpreting it as a foundation for mathematics that is independent of the homotopy interpretation of the HoTT Book though compatible with it. In particular, we interpret types as concepts; we have a slightly different understanding of subtypes and the Curry-Howard correspondence; and we offer a novel approach to the justification of the elimination rule for identity types in section 7 below (though it builds on a known mathematical result). These ideas are developed in detail in our papers downloadable from the project website: http://www.bristol.ac.uk/arts/research/current-projects/homotopy-type-theory/. While our ideas and views about some important matters differ from those presented in the HoTT Book the theory we present is essentially the same. Part I below introduces, explains and justifies the basic ideas, language and framework of HoTT including propositional logic, simple types, functions, quantification and identity types. In the subsequent parts of this Primer we extend the theory to predicate logic, the theory of the natural numbers, topology, the real numbers, fibre bundles, calculus and manifolds, and the very important `Univalence axiom