Philosophy of Mathematics seminar

David Corfield, Kent

Modal Homotopy Type Theory

Last year I published with OUP a book with this title, where I make the case that philosophy should look in the direction of this new logical system to expand its formal tools. In this talk I shall explain how modal homotopy type theory can usefully be understood as constructed in layers: types, dependent types, homotopy types, and modal types. For the philosophy of mathematics, one of the most interesting aspects of homotopy type theory is the way in which it embodies a structuralist outlook.