Philosophy of Mathematics Seminar (Monday - Week 7, MT18)

Homotopy Type Theory (HoTT) is a research programme in mathematics that connects algebraic topology with logic, computer science, and category theory. Its name derives from the way it integrates homotopy theory (which concerns spaces, points and paths) and formal type theory (as pioneered by Russell, Church, and Goedel, and developed in computer science) by interpreting types as spaces and terms of them as points in those spaces. Much of the interest in HoTT is due to the fact that it may be regarded as a ‘programming language for mathematics’, and it is formulated in a way that facilitates automated computer proof checking. HoTT is a ‘foundation for mathematics’ in the sense of a framework or language for mathematical practice. Within the language of HoTT it is possible to characterise mathematical structures such as natural numbers, real numbers, and groups, and to formalise proofs in homotopy theory. However, philosophers often mean something stronger by ‘foundation for mathematics’.They require a foundation to provide not just a language but also a conceptual and epistemological basis for mathematics, and moreover one that can be formulated without relying upon any other existing foundation. HoTT is interesting for philosophers because of its putative foundational status in this sense. However, there are many other philosophically rich aspects to HoTT. One is the way identity is treated in the theory, which is extremely different from traditional approaches and is what makes the theory in one sense 'intensional’. Another is that the Univalence Axiom in HoTT arguably (and according to Steve Awodey) expresses mathematical structuralism. Further matters of interest are that the theory is constructive and the way this interacts with its other features. Finally, type theory in general, and dependent types in particular provide a different formal approach to functions and quantication, and a different way of dealing with predication. In this talk I will present the basic ideas of HoTT paying particular attention to its novel conceptual foundations, and discussing a selection of philosophical issues in lesser and greater depth. (A free to download gentle introduction to HoTT is available here: http: //philsci-archive.pitt.edu/11157/)