Skip to main content
SpringerLink
Log in
Book cover

Reflections on the Foundations of Mathematics pp 101–136Cite as

Naïve Type Theory

  • Chapter
  • First Online:

Part of the book series: Synthese Library ((SYLI,volume 407))

Abstract

We introduce Type Theory, in its latest incarnation of Homotopy Type Theory, as an alternative to set theory as a foundation of Mathematics. We emphasize the naïve, intuitive understanding of Type Theory.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    This is also the title of a well known book by Halmos (1998).

  2. 2.

    We are not considering subtyping here, which can be understood as a notational device allowing the omission of implicit coercions.

  3. 3.

    I didn’t say they are all tautologies!

  4. 4.

    I am using here a record-like syntax for iterated Σ-types.

References

  • Altenkirch, T. (2019, to appear). The tao of types.

    Google Scholar 

  • Bertot, Y., & Castéran, P. (2013). Interactive theorem proving and program development: CoqArt – The calculus of inductive constructions. Berlin: Springer Science & Business Media.

    Google Scholar 

  • Brady, E. (2017). Type-driven development with Idris. Shelter Island: Manning Publications.

    Google Scholar 

  • Chlipala, A. (2013). Certified programming with dependent types: A pragmatic introduction to the Coq proof assistant. Cambridge: MIT Press.

    Book  Google Scholar 

  • Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2016). Cubical type theory: A constructive interpretation of the univalence axiom. arXiv preprint arXiv:1611.02108.

    Google Scholar 

  • Constable, R., et al. (1986). Implementing mathematics with the Nuprl proof development system. Prentice Hall.

    Google Scholar 

  • de Moura, L., Kong, S., Avigad, J., Van Doorn, F., & von Raumer, J. (2015). The lean theorem prover (system description). In International Conference on Automated Deduction (pp. 378–388). Springer.

    Google Scholar 

  • Halmos, P. R. (1998). Naive set theory. Springer-Verlag New York.

    Google Scholar 

  • Hofmann, M., & Streicher, T. (1998). The groupoid interpretation of type theory. Twenty-Five Years of Constructive Type Theory (Venice, 1995), 36, 83–111.

    Google Scholar 

  • Kapulkin, C., & Lumsdaine, P. L. (2012). The simplicial model of univalent foundations (after voevodsky). arXiv preprint arXiv:1211.2851.

    Google Scholar 

  • Kraus, N., & Sattler, C. (2015). Higher homotopies in a hierarchy of univalent universes. ACM Transactions on Computational Logic (TOCL), 16(2), 18:1–18:12.

    Google Scholar 

  • Licata, D. R., & Shulman, M. (2013). Calculating the fundamental group of the circle in homotopy type theory. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’13 (pp. 223–232), Washington, DC. IEEE Computer Society.

    Google Scholar 

  • Norell, U. (2008). Dependently typed programming in Agda. In P. Koopman, R. Plasmeijer, & D. Swierstra (Eds.), International school on advanced functional programming (pp. 230–266). Berlin/Heidelberg: Springer.

    Google Scholar 

  • Stump, A. (2016). Verified functional programming in Agda. San Rafael: Morgan & Claypool.

    Book  Google Scholar 

  • The Univalent Foundations Program. (2013). Homotopy type theory: Univalent foundations of mathematics (1st ed.). Princeton: Univalent Foundations program.

    Google Scholar 

Download references

Acknowledgements

There are very many people to thank: my colleagues from whom I learned very much and the students who attended my talks and courses and provided important feedback and comments. I would like to single out two people, who sadly passed away recently well before their time: Vladimir Voevodsky and Martin Hofmann. Vladimir basically invented Homotopy Type Theory and I have profited from many conversations with him and from his talks. Martin is a very good friend of mine and made many important contributions to type theory, one of them the groupoid interpretation of type theory which is now viewed as an early predecessor of HoTT. Both will be sorely missed.

Author information

Authors and Affiliations

  1. Functional Programming Laboratory, School for Computer Science, University of Nottingham, Nottingham, UK

    Thorsten Altenkirch

Authors
  1. Thorsten Altenkirch
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Thorsten Altenkirch .

Editor information

Editors and Affiliations

  1. Technical University of Berlin, Berlin, Germany

    Stefania Centrone

  2. University of Konstanz, Konstanz, Germany

    Deborah Kant

  3. University of Hamburg, Hamburg, Germany

    Deniz Sarikaya

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Altenkirch, T. (2019). Naïve Type Theory. In: Centrone, S., Kant, D., Sarikaya, D. (eds) Reflections on the Foundations of Mathematics. Synthese Library, vol 407. Springer, Cham. https://doi.org/10.1007/978-3-030-15655-8_5

Download citation

Publish with us

Policies and ethics

Search

Navigation