Chapter 2 notes
The definition of identity types, with their induction principle, is due to Martin-Löf . As mentioned in the notes to http://planetmath.org/node/87533Chapter 1, our identity types are those that belong to intensional type theory, by contrast with those of extensional type theory which have an additional “reflection rule” saying that if , then in fact . This reflection rule implies that all the higher groupoid structure collapses (see http://planetmath.org/node/87645Exercise 2.14), so for nontrivial homotopy we must use the intensional version. One may argue, however, that homotopy type theory is in another sense more “extensional” than traditional extensional type theory, because of the function extensionality and univalence axioms.
The proofs of symmetry (inversion) and transitivity (concatenation) for equalities are well-known in type theory. The fact that these make each type into a 1-groupoid (up to homotopy) was exploited in  to give the first “homotopy” style semantics for type theory.
The actual homotopical interpretation, with identity types as path spaces, and type families as fibrations, is due to , who used the formalism of Quillen model categories. An interpretation in (strict) -groupoids was also given in the thesis . For a construction of all the higher operations and coherences of an -groupoid in type theory, see  and .
Operations such as and , and one good notion of equivalence, were first studied extensively in type theory by Voevodsky, using the proof assistant Coq. Subsequently, many other equivalent definitions of equivalence have been found, which are compared in http://planetmath.org/node/87577Chapter 4.
The “computational” interpretation of identity types, transport, and so on described in §2.5 (http://planetmath.org/25thehighergroupoidstructureoftypeformers) has been emphasized by . They also described a “1-truncated” type theory (see http://planetmath.org/node/87580Chapter 7) in which these rules are judgmental equalities. The possibility of extending this to the full untruncated theory is a subject of current research.
The naive form of function extensionality which says that “if two functions are pointwise equal, then they are equal” is a common axiom in type theory, going all the way back to . Some stronger forms of function extensionality were considered in . The version we have used, which identifies the identity types of function types up to equivalence, was first studied by Voevodsky, who also proved that it is implied by the naive version (and by univalence; see §4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality)).
The univalence axiom is also due to Voevodsky. It was originally motivated by semantic considerations; see .
In the type theory we are using in this book, function extensionality and univalence have to be assumed as axioms, i.e. elements asserted to belong to some type but not constructed according to the rules for that type. While serviceable, this has a few drawbacks. For instance, type theory is formally better-behaved if we can base it entirely on rules rather than asserting axioms. It is also sometimes inconvenient that the theorems of §2.6 (http://planetmath.org/26cartesianproducttypes) to §2.13 (http://planetmath.org/213naturalnumbers) are only propositional equalities (paths) or equivalences, since then we must explicitly mention whenever we pass back and forth across them. One direction of current research in homotopy type theory is to describe a type system in which these rules are judgmental equalities, solving both of these problems at once. So far this has only been done in some simple cases, although preliminary results such as  are promising. There are also other potential ways to introduce univalence and function extensionality into a type theory, such as having a sufficiently powerful notion of “higher quotients” or “higher inductive-recursive types”.
The simple conclusions in §2.12 (http://planetmath.org/212coproducts) to §2.13 (http://planetmath.org/213naturalnumbers) such as “ and are injective and disjoint” are well-known in type theory, and the construction of the function is the usual way to prove them. The more refined approach we have described, which characterizes the entire identity type of a positive type (up to equivalence), is a more recent development; see e.g. .
The type-theoretic axiom of choice (2.15.6) (http://planetmath.org/215universalproperties#S0.E4) was noticed in William Howard’s original paper  on the propositions-as-types correspondence, and was studied further by Martin-Löf with the introduction of his dependent type theory. It is mentioned as a “distributivity law” in Bourbaki’s set theory .
For a more comprehensive (and formalized) discussion of pullbacks and more general homotopy limits in homotopy type theory, see . Limits of diagrams over directed graphs are the easiest general sort of limit to formalize; the problem with diagrams over categories (or more generally -categories) is that in general, infinitely many coherence conditions are involved in the notion of (homotopy coherent) diagram. Resolving this problem is an important open question in homotopy type theory.
- 1 Jeremy Avigad and Krzysztof Kapulkin and Peter LeFanu Lumsdaine. Homotopy limits in Coq, 2013. \hrefhttp://arxiv.org/abs/1304.0680/arXiv:1304.0680.
- 2 Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146:45–55 2009
- 3 van den Berg,Benno and Garner,Richard. Types are weak -groupoids. Proceedings of the London Mathematical Society, 102:370–394 2011,Bdsk-Url-1
- 4 Nicolas Bourbaki, Theory of Sets Hermann,Paris,1968
- 5 Garner,Richard. On the strength of dependent products in the type theory of Martin-Löf. Annals of Pure and Applied Logic, 160:1–12 2009,Bdsk-Url-1
- 6 Howard,William A.. The formulae-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic,Lambda Calculus and Formalism,pages 479–490. Academic Press, 1980.
- 7 Hofmann,Martin and Streicher,Thomas. The groupoid interpretation of type theory. In Twenty-five years of constructive type theory (Venice,1995),volume 36 of Oxford Logic Guides, pages 83–111. Oxford University Press, 1998.
- 8 Chris Kapulkin and Peter LeFanu Lumsdaine and Vladimir Voevodsky. The Simplicial Model of Univalent Foundations, 2012. \hrefhttp://arxiv.org/abs/1211.2851/arXiv:1211.2851.
- 9 Licata,Daniel R. and Harper,Robert. Canonicity for 2-dimensional type theory. In emphProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 337–348ACM, .
- 10 Licata,Daniel R. and Harper,Robert. Canonicity for 2-dimensional type theory. In emphProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 337–348ACM, .
- 11 Daniel R. Licata and Michael Shulman. Calculating the Fundamental Group of the Circle in Homotopy Type Theory. In emphLICS 2013: Proceedings of the Twenty-Eighth Annual ACM/IEEE Symposium on Logic in Computer Science, .
- 12 Martin-Löf,Per. An intuitionistic theory of types. In Twenty-five years of constructive type theory (Venice,1995),volume 36 of Oxford Logic Guides, pages 127–172. Oxford University Press, 1998.
- 13 Michael A. Warren. Homotopy Theoretic Aspects of Constructive Type Theory. PhD thesis, Carnegie Mellon University, 2008.
- 14 Lumsdaine,Peter LeFanu. Weak omega-categories from intensional type theory. Typed lambda calculi and applications, 6:1–19 2010,Bdsk-Url-1
- 15 Whitehead,Alfred North and Russell,Bertrand, Principia mathematica,3 vol.s Cambridge University Press,1910–1913; Second edition,1925–1927
|Title||Chapter 2 notes|