Meet the Project: 'Homotopy Type Theory and Univalent Foundations'
This month, we're sitting down with the 2018/19 CAS project leaders and fellows to hear about their plans for their year at the Centre. Today: Homotopy Type Theory and Univalent Foundations.
Homotopy type theory is -- in the grand scope of science -- still a ‘toddler.’
Marc Bezem and Bjørn Ian Dundas, respectively professors of informatics and mathematics at the University of Bergen (UiB), are spending a year at the Centre for Advanced Study (CAS) to help the theory grow up.
Their CAS project, Homotopy Type Theory and Univalent Foundations, explores the titular theory. It emerged in the 2000s, building on existing theories in computer science and mathematics. As with any new theory, there are still several kinks that need to be straightened out.
‘Since the modern society depends on mathematics, secure foundations are important,’ Bezem and Dundas write in the project abstract. ‘In the digital era we have powerful tools for verifying (and to some extent generating) formal mathematical proofs. The central challenge is finding a language that has sufficient expressive power, and at the same time can be mechanically processed in an efficient way. Homotopy type theory addresses exactly this challenge.’
The CAS project is something of a follow-up to ‘A Special Year on Univalent Foundations of Mathematics,’ hosted at the Institute for Advanced Study in Princeton, New Jersey, during the 2012/13 academic year. Bezem and several of the other scholars who participated in that programme will also spend time at CAS this academic year.
The scholars, most of whom are in the fields of computer science and mathematics, represent institutions in Canada, Germany, Norway, Sweden, the United Kingdom, and the United States. In addition to a core of senior scholars, the project includes several junior academics and Ph.D. students who soon may be the ones to take homotopy type theory from toddler to teenager.
Bezem and Dundas sat down shortly after arriving at CAS to discuss their plans for the project. Read their thoughts below.
Read more about the project, Homotopy Type Theory and Univalent Foundations, here.
- Tell us about your project. What do you hope to accomplish during your year at CAS?
Marc Bezem: We will further develop homotopy type theory, and we will do some challenging formal verifications.
- Further develop -- so where is the theory today, and where would you like to see it go?
Bjørn Ian Dundas: It’s not quite in its infancy. Should we say that it’s a toddler? It has existed for a number of years, dating back to 2006, 2009. That means there are some things that are already fixed. Still, there are fundamental questions that need to be addressed.
- Why is CAS the right arena for this type of research project?
Bezem: Here we have the peace to commit all our time to doing research. That is one point that is important for Bjørn and me. Another important point is that we can invite specialists from all over the world to do research with us.
- How did the two of you end up working together?
Bezem: -- I had to prepare for the Special Year at the Institute for Advanced Study in Princeton on homotopy type theory. So the same topic as here, but back then -- five years ago -- it was in its infancy.
Dundas: That year of course was on a totally different scale from what we’re seeing here at CAS, but it’s of a similar nature where you gather experts and work together. We could certainly say that this year was inspired by that year, although with a much smaller scope.
Bezem: We also discovered that the topic is truly interdisciplinary, since the languages we speak are completely different.
Dundas: That is a daily problem, actually.
Bezem: The point of view of the logician is rather different from the point of view of the working mathematician on this subject. But that only makes it interesting.
- How did you decide which scholars to invite?
Dundas: We started from a core of more senior scientists. Of course they have busy schedules, so you have to build around that. There are several people who were there at the Special Year at Princeton who are coming here as well. In addition to that, there are two Ph.D. students.
Bezem: We asked for advice from the senior scientists -- who would you recommend to invite? Who would you like to collaborate with?
- You had invited Vladimir Voevodsky, one of the founding fathers of homotopy type theory, who died last year. How does that loss affect the development of the field?
Bezem: It’s an enormous loss. He was full of ideas and a strong drive to further develop the subject.
Dundas: It’s a tragic loss. But there are definitely other people who are stepping in and doing a great job. There is a wide range of people coming in right now that are taking over and building the theory further.
Bezem: The subject is larger than one man, as they often say.
- Practically speaking, how will the members of your project work together this year?
Dundas: Blackboard interaction is perhaps the key way of getting ideas across. Once you’re two or three people at a blackboard, ideas start flourishing. We play off each other better. That is definitely one of the amazing things about ‘doing’ mathematics. When you’re more than one person at a blackboard, I feel that I say things that I wouldn’t have said unless the other people had said something. It’s on speed compared to when you just sit and think by yourself. Of course 90 percent of what is said is junk, but 10 percent can be really good and will be carried forward. Actually being in the same room is an entirely different thing that skyping or writing emails. That is what makes an environment like this a very good one.
Once a theory has been developed, new axioms show up, and then there is always the question of consistency. Can we use these axioms all together without running into contradictions? This has not been sorted out for all combination of axioms yet. The stakes are rather high. It is very important to avoid contradictions. That is one important technical problem.
Another important technical problem is that we have a new theory in which we represent all mathematics. Then the basic question is ‘How do you actually do that?’ Even more importantly, if you do that, is the way you represent mathematics exactly as it had been meant? Is the new representation faithful with respect to the old one?
Dundas: One of the things we’re aiming at is automatic verification of proofs. But if the user can cast any doubt on whether the proof is really a proof of what you were asked to prove, that would be a very, very bad thing. The relevance of the field rests on this mirroring.
I like to think of it as a game where you’re given rules. You have this card, you have that card, and you follow the logical rules -- the axioms. But as Marc said, you better not have so many rules that they actually contradict themselves. It must be a logical game, and it must also be relevant to what it’s supposed to do.
- Where do you hope you’ll be in one year?
Dundas: There are some precise questions that we’re working on. Of course we would like to see these problems solved, but we have to be realistic. What might be is that, OK, we didn’t solve it, but we understood it way better, and it actually turned out that if you want to prove this, then you also have to understand that.
You have these goals into the future, and you’re working toward them, but of course you don’t know all the valleys and mountains that are in between. I should say that we should understand the terrain toward our more general goals way, way better.
Bezem: This goes by trial and error. You must have a little bit of luck. In the shorter term, it’s very hard to predict. It’s like the weather. The weather in 10 days is harder to predict than the climate over 30 years. So the ‘weather’ in one year, let’s say, is even harder to predict.
Dundas: Of course it is also about building competence --
Bezem: -- particularly for the young people.
Dundas: Given that the field is so young, we’re still in a phase where we’re exploring, and there are probably quite a number of false leads. There are ideas up there in front that we’re heading toward, and we’re probably going to go down some blind alleys occasionally, but hopefully we’ll press the field forward. It’s called fundamental research!
Here's what some of the fellows participating in Homotopy Type Theory and Univalent Foundations have planned for their year at CAS:
'During my stay at CAS, I am implementing results from mathematics in homotopy type theory. In other words, I am translating mathematical statements and proofs into something a computer can understand. More precisely, I am trying to make the computer consider the problem "What happens if we try talking about sets with a negative number of elements?"'
'My main goal at the Centre will be to verify the proofs in a preprint of mine on algebraic K-theory by translating them into the formal language of Univalent Mathematics, thereby allowing the computer to verify them. I hope to submit the paper for publication along with the formal verification.'
Anthony Bordg, postdoctoral fellow at the University of Cambridge:
'This year at CAS I will investigate two aspects of the Univalent Foundations of mathematics. First, I will explore some model-theoretic questions that arise in relation to the Univalent Foundations. Second, I will try to tackle some challenges faced by researchers checking mathematics with computers in these foundations.'