Abstract
The present paper investigates the use of impredicative methods for the construction of inductive types in homotopy type theory. Inductive types have been constructed impredicatively in other systems of type theory in the past, but these fail to have the correct rules. Using new methods, the paper shows how to repair these prior constructions, and extend the impredicative methodology to include also the newly discovered higher inductive types that form the basis of the recent applications in homotopy theory. This present work refines and extends the traditional logistic approach to foundations of mathematics to encompass both arithmetic and geometry in a comprehensive logistic system that also admits a computational implementation on modern computing machines. The connection to the idea of mathesis universalis is thus quite direct.
Thanks to Dr. Stefana Centrone for organizing a most stimulating meeting. Some parts of the work reported here were done jointly with my student Sam Speight and collaborators Jonas Frey and Pieter Hofstra. This research was partially supported by the U.S. Air Force Office of Scientific Research through MURI grant FA9550-15-1-0053. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR.
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
Similar content being viewed by others
Notes
- 1.
See Lawvere (1970) for a closely related principle.
- 2.
There is a technical question related to the selection of path objects and diagonal fillers as interpretations of I d A-types and elimination J-terms in a “coherent” way, i.e. respecting substitution of terms for variables; various solutions have been given, including Warren (2008), van den Berg and Garner (2012), Voevodsky (2009), Lumsdaine and Warren (2015), and Awodey (2018a).
- 3.
- 4.
- 5.
A map f : A → B induces a map on identities, taking each p : I d A(a, b) to a term in I d B(fa, fb) which we here write f ! p (see The Univalent Foundations Program 2013, ch. 2). The equation for l o o p is often taken in propositional form.
References
Awodey, S. (2000). Topological representation of the lambda-calculus. Mathematical Structures in Computer Science, 1(10), 81–96.
Awodey, S. (2018a). Natural models of homotopy type theory. Mathematical Structures in Computer Science, 28(2), 241–286.
Awodey, S. (2018b). Univalence as a principle of logic. Indagationes Mathematicae, Special Issue – L.E.J. Brouwer After 50 Years, 29, 1497–1510.
Awodey, S., & Bauer, A. (2004). Propositions as [types]. Journal of Logic and Computation, 14(4), 447–471.
Awodey, S., & Butz, C. (2000). Topological completeness for higher-order logic. Journal of Symbolic Logic, 3(65), 1168–1182.
Awodey, S., & Warren, M. (2009). Homotopy-theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society, 146(1), 45–55.
Awodey, S., Gambino, N., & Sojakova, K. (2012). Inductive types in Homotopy Type Theory. In Logic in Computer Science (LICS 2012) (pp. 95–104). IEEE Computer Society.
Awodey, S., Gambino, N., & Sojakova, K. (2017). Homotopy-initial algebras in type theory. Journal of the ACM, 63(6), 51:1–51:45.
Awodey, S., Frey, J., & Speight, S. (2018). Impredicative encodings of (higher) inductive types. In Proceedings of the 2018 33rd Annual IEEE/ACM Symposium on Logic in Computer Science (LICS 2018). IEEE Computer Society.
Coq Development Team. (2012). The Coq proof assistant reference manual, version 8.4pl3. INRIA. Available at http//:coq.inria.fr
Coquand, T., & Huet, G. (1988). The calculus of constructions. Information and Computation, 76(2), 95–120.
Frege, G. (1879). Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle: Verlag Louis Nebert.
Gambino, N., & Garner, R. (2008). The identity type weak factorisation system. Theoretical Computer Science, 409(3), 94—109.
Hofmann, M., & Streicher, T. (1998). The groupoid interpretation of type theory. In Twenty-five years of constructive type theory 1995 (Volume 36 of Oxford logic guides, pp. 83–111). Oxford University Press.
Hyland, J. M. E. (1988). A small complete category. Annals of Pure and Applied Logic, 40(2), 135–165.
Kamareddine, F. D., Laan, T., & Nederpelt, R. P. (2004). A modern perspective on type theory: From its origins until today. Netherlands: Springer.
Lawvere, F. W. (1970). Equality in hyperdoctrines and comprehension schema as an adjoint functor. In A. Heller (Ed.), Proceedings of the AMS Symposium on Pure Mathematics (Vol. XVII, pp. 1–14).
Licata, D., & Shulman, M. (2013). Calculating the fundamental group of the circle in Homotopy Type Theory. In Logic in Computer Science (LICS 2013) (pp. 223–232). IEEE Computer Society.
Lumsdaine, P. L. (2010). Weak ω-categories from intensional type theory. Logical Methods in Computer Science, 6, 1–19.
Lumsdaine, P. L., & Warren, M. A. (2015). The local universes model: An overlooked coherence construction for dependent type theories. ACM Transactions on Computational Logic, 16(3), 23:1–23:31.
Martin-Löf, P. (1984). Intuitionistic type theory (Notes by G. Sambin of a series of lectures given in Padua, 1980). Naples: Bibliopolis.
Shulman, M. (2018). Impredicative encodings, part 3. Post on the Homotopy Type Theory blog.
Sojakova, K. (2014). Higher inductive types as homotopy-initial algebras (Technical report CMU-CS-14-101), Carnegie Mellon University. Available at http://reports-archive.adm.cs.cmu.edu/
The Univalent Foundations Program, Institute for Advanced Study. (2013). Homotopy type theory – Univalent foundations of mathematics. Univalent Foundations Project.
vanden Berg, B., & Garner, R. (2011). Types are weak ω-groupoids. Journal of the London Mathematical Society, 102(2), 370–394.
van den Berg, B., & Garner, R. (2012). Topological and simplicial models of identity types. ACM Transactions on Computational Logic, 13(1), 1–44.
Voevodsky, V. (2009). Notes on type systems. Available from the author’s web page.
Warren, M. (2008). Homotopy-theoretic aspects of constructive type theory. Ph.D. thesis, Carnegie Mellon University.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Awodey, S. (2019). Mathesis Universalis and Homotopy Type Theory. In: Centrone, S., Negri, S., Sarikaya, D., Schuster, P.M. (eds) Mathesis Universalis, Computability and Proof. Synthese Library, vol 412. Springer, Cham. https://doi.org/10.1007/978-3-030-20447-1_3
Download citation
DOI: https://doi.org/10.1007/978-3-030-20447-1_3
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-20446-4
Online ISBN: 978-3-030-20447-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)