Abstract
Martin-Löf’s Extensional Type Theory (ETT) has a straighforward semantics in the category Set of sets and functions and actually in any locally cartesian closed category with a natural numbers object (nno), e.g., in any elementary topos with a nno. Dependent products are interpreted by right adjoints to pullback functors, and extensional identity types are interpreted as diagonals in slice categories as explained, e.g., in [4].
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Since, otherwise, one could recursively separate the r.e. sets \(A_{0} =\{ n \in \mathbb{N}\mid \{n\}(n) = 0\}\) and \(A_{1} =\{ n \in \mathbb{N}\mid \{n\}(n) = 1\}\) which can be seen as follows. For natural numbers n consider the primitive recursive predicate \(P_{n}(k) \equiv T(n,n,k) \rightarrow U(k) = 0\). If n ∈ A 0 then \(\mathcal{T} \vdash \forall k.P_{n}(k)\) and if n ∈ A 1 then \(\mathcal{T} \vdash \neg \forall k.P_{n}(k)\) and thus \(\mathcal{T}\nvdash \forall k.P_{n}(k)\). Now let f be a total recursive function with f(n) = 0 if and only if \(\mathcal{T} \vdash \forall k.P_{n}(k)\), which exists since the set of \(\Pi _{1}^{0}\)-sentences provable in T is assumed to be decidable. But then f(n) = 0 if n ∈ A 0 and f(n) ≠ 0 if n ∈ A 1, i.e., f recursively separates the sets A 0 and A 1, which is known to be impossible.
- 2.
This has to be seen in sharp contrast with the fact that most known non-syntactic models for ITT + UA (as, e.g., the groupoid and the simplicial sets model) validate the same propositions of BTT as the model in Set does.
References
Univalent Foundations Project, in Homotopy Type Theory – Univalent Foundations of Mathematics (Institute for Advanced Study, Princeton, 2013). http://homotopytypetheory.org/book/
M. Hofmann, Extensional Concepts in Intensional Type Theory PhD thesis, University of Edimburgh, 1995. http://www.era.lib.ed.ac.uk/bitstream/1842/399/2/ECS-LFCS-95-327.PDF
M. Hofmann, T. Streicher, The groupoid interpretation of type theory, in Twenty-Five Years of Martin Löf Type Theory (Venice, 1995). Oxford Logic Guides, vol. 36 (OUP, New York, 1998), pp. 83–111
T. Streicher, Semantics of Type Theory (Birkhäuser, Boston, 1991)
T. Streicher, Investigations into intensional type theory, Habilitation Thesis Ludwig-Maximilans-Universität Munich, 1993. http://www.mathematik.tu-darmstadt.de/;~streicher/HabilStreicher.pdf.
J. van Oosten, Realizability. An Introduction to Its Categorical Side (Elsevier, Oxford, 2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Streicher, T. (2015). How Intensional Is Homotopy Type Theory?. In: González, M., Yang, P., Gambino, N., Kock, J. (eds) Extended Abstracts Fall 2013. Trends in Mathematics(). Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-21284-5_20
Download citation
DOI: https://doi.org/10.1007/978-3-319-21284-5_20
Publisher Name: Birkhäuser, Cham
Print ISBN: 978-3-319-21283-8
Online ISBN: 978-3-319-21284-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)