2026-06-10, Wednesday (opens in new tab)

Visiting the Mittag-Leffler institute this week. A pleasant stay thus far, with lots of great researchers gathered to push towards formalisation of ∞-categories. Surprising amount of progress is being made here. Especially in the synthetic methods. Agda, with its flexible type system and liberal collection of extension (not unlike GHC), is at an advantage here. I have been playing around with a synthetic ∞-category library by Sam, which seems promising. We are not quite at the levels of conve...