Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 19, 2016

The HoTT Effect

Posted by David Corfield

Martin-Löf type theory has been around for years, as have category theory, topos theory and homotopy theory. Bundle them all together within the package of homotopy type theory, and philosophy suddenly takes a lot more interest.

If you’re looking for places to go to hear about this new interest, you are spoilt for choice:

For an event which delves back also to pre-HoTT days, try my

CFA: Foundations of Mathematical Structuralism

12-14 October 2016, Munich Center for Mathematical Philosophy, LMU Munich

In the course of the last century, different general frameworks for the foundations of mathematics have been investigated. The orthodox approach to foundations interprets mathematics in the universe of sets. More recently, however, there have been other developments that call into question the whole method of set theory as a foundational discipline. Category-theoretic methods that focus on structural relationships and structure-preserving mappings between mathematical objects, rather than on the objects themselves, have been in play since the early 1960s. But in the last few years they have found clarification and expression through the development of homotopy type theory. This represents a fascinating development in the philosophy of mathematics, where category-theoretic structural methods are combined with type theory to produce a foundation that accounts for the structural aspects of mathematical practice. We are now at a point where the notion of mathematical structure can be elucidated more clearly and its role in the foundations of mathematics can be explored more fruitfully.

The main objective of the conference is to reevaluate the different perspectives on mathematical structuralism in the foundations of mathematics and in mathematical practice. To do this, the conference will explore the following research questions: Does mathematical structuralism offer a philosophically viable foundation for modern mathematics? What role do key notions such as structural abstraction, invariance, dependence, or structural identity play in the different theories of structuralism? To what degree does mathematical structuralism as a philosophical position describe actual mathematical practice? Does category theory or homotopy type theory provide a fully structural account for mathematics?

Confirmed Speakers:

  • Prof. Steve Awodey (Carnegie Mellon University)
  • Dr. Jessica Carter (University of Southern Denmark)
  • Prof. Gerhard Heinzmann (Université de Lorraine)
  • Prof. Geoffrey Hellman (University of Minnesota)
  • Prof. James Ladyman (University of Bristol)
  • Prof. Elaine Landry (UC Davis)
  • Prof. Hannes Leitgeb (LMU Munich)
  • Dr. Mary Leng (University of York)
  • Prof. Øystein Linnebo (University of Oslo)
  • Prof. Erich Reck (UC Riverside)

Call for Abstracts:

We invite the submission of abstracts on topics related to mathematical structuralism for presentation at the conference. Abstracts should include a title, a brief abstract (up to 100 words), and a full abstract (up to 1000 words), blinded for peer review. Authors should send their abstracts (in pdf format), together with their name, institutional affiliation and current position to We will select up to five submissions for presentation at the conference. The conference language is English.

Dates and Deadlines:

  • Submission deadline: 30 June, 2016
  • Notification of acceptance: 31 July, 2016
  • Registration deadline: 1 October, 2016
  • Conference: 12 - 14 October, 2016
Posted at May 19, 2016 12:57 PM UTC

TrackBack URL for this Entry:

3 Comments & 0 Trackbacks

Re: The HoTT Effect

I have a somewhat jaded view of the burst of popularity of homotopy type theory within mathematics, even though it’s a good thing overall.

But I feel better about what this burst of popularity might do to philosophy. The philosophy of mathematics, unlike mathematics itself, has been stuck in contemplating old ideas on logic for far too long. (I don’t need to tell you that.) If more philosophers start trying to learn homotopy type theory, a bunch are bound to learn about homotopy theory, topos theory, nn-category theory, and other branches of math that have profound new things to say about concepts like equality, numbers, propositions, logical operations, space and the like… where ‘new’ means post-1950s. This could really enliven the conversation in philosophy.

Posted by: John Baez on May 26, 2016 8:01 PM | Permalink | Reply to this

Re: The HoTT Effect

In a more reasonable world we would have more philosophers sniffing around constructive type theory, theoretical computer science and (higher) category theory for many years by now, pushing for dialogue, and making more of a contribution to the rise of such a new language.

Some reflection on the cause of this general slowness wouldn’t go amiss.

Anyway looking ahead, there should be some fun to be had, now with the chance of an audience. I’m looking into modal type theory and type theoretic constructions in the context of a group at the moment. Group invariants and necessity are manifestations of the same thing.

Posted by: David Corfield on May 26, 2016 9:30 PM | Permalink | Reply to this

Re: The HoTT Effect

For lazy people, the link to the event in Munich in October is here.

Posted by: Manuel Bärenz on August 23, 2016 9:00 PM | Permalink | Reply to this

Post a New Comment