StockholmGoteborgMeeting251029
Venue
Room Analysen, EDIT building, Chalmers campus, Göteborg
Schedule
| 11:40 - 12:10 | Anders Mörtberg |
| Lunch | |
| 13:20 - 13:50 | David Wärn |
| 14:00 - 14:30 | Peter LeFanu Lumsdaine |
| 14:40 - 15:10 | Andreas Abel |
| Coffee | |
| 15:50 - 17:00 | Discussion: what are the most important research directions and open problems in type theory? Please add your suggestions here. |
| Slides and notes from the discussion. | |
| 18:00 | Dinner Andrum (map) |
Anders Mörtberg: The Serre finiteness theorem formalized in Cubical Agda
In the early 1950s Jean Pierre Serre proved a remarkable result establishing that the homotopy groups of spheres are finite, except for a few special cases. A synthetic proof in HoTT of this landmark result in algebraic topology was announced by Barton and Campion in 2022. This quickly inspired Ljungström and myself to team up with Barton and Milner at CMU to embark on an extensive project to formalize the proof in Cubical Agda. About a month ago, this formalization was finally completed.
The proof of Barton and Campion is very interesting not only as it establishes that Serre's classical result can be proved synthetically in HoTT, but also because it is fully constructive. The statement of their theorem is that all homotopy groups of spheres are finitely presented, which means that we can (in principle) compute all of them by normalizing the proof terms in Cubical Agda. The proof is also quite elementary compared to Serre's proof and its formalization was fun because it involved not only the formalization of lots of synthetic algebraic topology, but also linear algebra and diagonalization of integer matrices. In the talk I will outline the proof and discuss various simplifications that we found when formalizing it.
David Wärn: Axioms for higher category theory?
Higher category theory is increasingly being developed and applied using informal language that is intrinsically homotopical and model-independent. In this talk I will argue that this practice can naturally be carried out inside of HoTT together with a collection of axioms describing the wild (∞,1)-category of small (∞,1)-categories. We circumvent the complexities of directed type theory and multimodal type theory by interpreting types as spaces rather than categories. The collection of axioms is otherwise similar to that recently introduced by Cisinski, Cnossen, Nguyen, and Walde.
Peter LeFanu Lumsdaine: Formalising recursive mathematics in Lean and Rocq
I’ll present an ongoing project, jww Sina Hazratpour, on formalising recursive mathematics.
Precisely, by “recursive mathematics”, we mean a type theory conservative over primitive recursive arithmetic (PRA) — in categorical terms, the internal language of a locos or arithmetic universe — but extended with limited function types and inductive types for better expressivity.
The project involves two roughly parallel formalisations: one in Rocq, using Rocq’s ambient CIC as a logical framework for the finitistic type theory; and one in Lean, with categorical models (locoses/AU’s) explicitly formalised, and the finitistic type theory presented as a DSL interpreted into these via Lean’s metaprogramming.
Andreas Abel: Type Theory Incarnate
Type theory is first a mathematical structure, but to affect the world, it needs an implementation. We could also say it needs to incarnate; and that is where things get dirty.
In this talk, I will review the layers of incarnated type theory that take us further and further away from the core, that is, from semantics and rules. I will further review the status of some aspects of the incarnation Agda, and make a plea to extend the reach of mathematical investigation into more of its layers.