Type Theory and Homotopy

In Peter Dybjer, Sten Lindström, Erik Palmgren & Göran Sundholm (eds.), Epistemology Versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf. Dordrecht, Netherland: Springer. pp. 183-201 (2012)
  Copy   BIBTEX

Abstract

The purpose of this informal survey article is to introduce the reader to a new and surprising connection between Logic, Geometry, and Algebra which has recently come to light in the form of an interpretation of the constructive type theory of Per Martin-Löf into homotopy theory and higher-dimensional category theory.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 100,448

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Homotopy theoretic models of identity types.Steve Awodey & Michael Warren - 2009 - Mathematical Proceedings of the Cambridge Philosophical Society 146:45–55.
Constructive mathematics and equality.Bruno Bentzen - 2018 - Dissertation, Sun Yat-Sen University
Truth and proof in intuitionism.Dag Prawitz - 2012 - In Peter Dybjer, Sten Lindström, Erik Palmgren & B. Göran Sundholm (eds.), Epistemology versus Ontology: Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf. Springer. pp. 45–67.
Does Homotopy Type Theory Provide a Foundation for Mathematics?Stuart Presnell & James Ladyman - 2018 - British Journal for the Philosophy of Science 69 (2):377-420.

Analytics

Added to PP
2010-10-11

Downloads
142 (#156,474)

6 months
12 (#277,938)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Steve Awodey
Carnegie Mellon University

Citations of this work

Structuralism, Invariance, and Univalence.Steve Awodey - 2014 - Philosophia Mathematica 22 (1):1-11.
Informal proof, formal proof, formalism.Alan Weir - 2016 - Review of Symbolic Logic 9 (1):23-43.
Identity in Martin‐Löf type theory.Ansten Klev - 2021 - Philosophy Compass 17 (2):e12805.
Maddy On The Multiverse.Claudio Ternullo - 2019 - In Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer Verlag. pp. 43-78.

View all 11 citations / Add more citations

References found in this work

Homotopy theoretic models of identity types.Steve Awodey & Michael Warren - 2009 - Mathematical Proceedings of the Cambridge Philosophical Society 146:45–55.
Wellfounded trees in categories.Ieke Moerdijk & Erik Palmgren - 2000 - Annals of Pure and Applied Logic 104 (1-3):189-218.
Generalised algebraic theories and contextual categories.John Cartmell - 1986 - Annals of Pure and Applied Logic 32:209-243.

Add more references