Project Update: 'Homotopy Type Theory and Univalent Foundations'

Following a well-deserved winter break, the fellows have returned to CAS to continue their research.

We checked in with the members of the project Homotopy Type Theory and Univalent Foundations to learn how their work is going, their thoughts on the stay so far, and their plans for the spring.

Here’s a recap: Homotopy Type Theory and Univalent Foundations is a mathematics and computer science project that is aimed at further developing a theory that emerged in the early 2000s. The project is led by Marc Bezem and Bjørn Ian Dundas, respectively professors of informatics and mathematics at the University of Bergen (UiB).

The project began in earnest during a kickoff conference early last fall, during which fellows gave an overview of their research and expertise. Since then, the fellows have taken over the third floor of CAS’ premises in Oslo, filling every inch of whiteboard space that the Centre has to offer with mathematical proofs.

Since both Bezem and Dundas are based in Bergen, they don’t have the same extensive local academic network that a researcher based in the Oslo region might have. So instead of a constantly rotating cast of researchers, their project has featured a smaller number of fellows who have been able to stay for longer periods of time.

That structure has influenced the topics that the group has focused its attention on, Bezem and Dundas said.

‘Given that we’re seven-eight people, each individual person is going to put his or her stamp on the programme when they’re here,’ Dundas said. ‘There was perhaps more of a homotopy theory drive for a while at the end of the fall, and now we’re perhaps in a more computer science, logician mode. It depends on the fellows.’

Of course, rethinking mathematics from a new theoretical perspective is no small task, and Bezem and Dundas said they know that their work will continue long after their year at CAS -- and likely for years after they both retire.

‘Throughout history, there have been many examples of “rewriting mathematics” from a new perspective,’ Bezem said. ‘Some of them are too grand to serve as a comparison. This is true of Euclid's Elements, which aimed at encompassing most known mathematics of that time. A good two millennia after Euclid, there has of course come a lot more mathematics, which perhaps explains the difficulty of the Bourbaki project -- a group of top mathematicians still working after 60 years.’

In addition to research meant to benefit the development of homotopy type theory long term, the fellows are also working on several shorter-term projects. One such project is a book on symmetry in mathematics. The book will explain abstract algebra from the univalent perspective to the mathematical community at large, but could also be used as a textbook at the undergraduate level, Bezem and Dundas said.

‘It’s actually a different view on the stuff that we train our students on, and that change of point of view has ramifications which I think are very, very interesting,’ Dundas said. ‘We’re trying to make an outreach toward the mainstream academic curriculum. As such it’s a mix between breaking new ground and tilling up old fields.’

Read more about the project, Homotopy Type Theory and Univalent Foundations, here.

Several fellows have already concluded their stay at CAS. Here's what some of them them had to say about their time at the Centre:

Stefano Piceghello, Ph.D. student at the University of Bergen (UiB):

 

'I'm investigating how coherence theorems in category theory fit in the new framework of homotopy type theory and univalent foundations, and at the same time formalising the newly produced proofs so that a computer can verify them. My stay at CAS has allowed me to discuss and share my work with other fellows and guests, from whom I have received relevant input and further insight.'

Chris Kapulkin, assistant professor of mathematics at the University of Western Ontario:

 

'My work spans many aspects of homotopy type theory and higher category theory. CAS provided me with remarkable conditions to work effectively at numerous projects. During just a two-month stay, I managed to significantly advance three of them, related to cubical sets, meta-theory of type theory, and computational aspects, and I hope to make the resulting preprints available shortly.'

The project is also welcoming new fellows this spring. Here's what some of them have planned for their stay:

Steve Awodey, professor of philosophy and mathematics at Carnegie Mellon University:

 

'In the past, I have studied the connection between homotopy theory and type theory. While at CAS, I will continue this by focusing on the connection between models of homotopy theory and models of type theory, specifically Quillen model structures and topos models of type theory.  This is part of my recent project to learn more about higher topos theory, which seems to me to unify past and present (and maybe future!) work in this area.'

André Joyal, professor emeritus of mathematics at the Université du Québec à Montréal:

 

'My goal this spring will be to complete a paper on the connection between homotopy type theory, higher topos theory and Goodwillie's calculus in collaboration with Mathieu Anel, Georg Biedermann, and Eric Finster. It will be unifying Goodwillie's calculus with Weiss's calculus.'