Ladyman, James and Presnell, Stuart (2014) A Primer on Homotopy Type Theory Part 1: The Formal Type Theory. UNSPECIFIED.
![[img]](https://philsci-archive.pitt.edu/style/images/fileicons/application_pdf.png)
|
PDF
HTT_Primer-PART-1.pdf Download (581kB) |
Abstract
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'
| Export/Citation: | EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL |
| Social Networking: |
| Item Type: | Other | |||||||||
|---|---|---|---|---|---|---|---|---|---|---|
| Creators: |
|
|||||||||
| Keywords: | Homotopy Type Theory | |||||||||
| Depositing User: | James Ladyman | |||||||||
| Date Deposited: | 19 Nov 2014 21:52 | |||||||||
| Last Modified: | 19 Nov 2014 21:52 | |||||||||
| Item ID: | 11157 | |||||||||
| Date: | 18 November 2014 | |||||||||
| URI: | https://philsci-archive.pitt.edu/id/eprint/11157 |
Monthly Views for the past 3 years
Monthly Downloads for the past 3 years
Plum Analytics
Actions (login required)
 |
View Item |
![[feed]](http://philsci-archive.pitt.edu/style/images/feed-icon-32x32.png){kind=icon}