StockholmGoteborgMeeting230412
Stockholm–Göteborg meeting on Wednesday, 12 April 2023 in Göteborg
Program
| 11:15–11:45 | arrive + time for discussions |
| 11:45–12:15 | Ivan Di Liberti |
| 12:15–14:00 | lunch break + time for discussions |
| 14:00–14:30 | David Wärn |
| 14:30–15:00 | Axel Ljungström |
| 15:00–15:30 | coffee break |
| 15:30–16:00 | Taichi Uemura |
| 16:00–16:30 | Felix Cherubini |
| 17:15 | dinner / pub evening at John Scott’s Palace (map) |
The talks are in EDIT room Analysen.
Abstracts
Ivan Di Liberti — Lindström in fabula
Lindström-type theorems are a paradigm of theorems that characterise fragments of logic among other logical system by identifying pivotal properties. The original theorem due to Lindström identifies first order logic as the minimal logic enjoying both compactness and Löwenheim-Skolem theorem. After an historical overview of Lindström-type theorems, we will see its incarnation in the 2-category of topoi, where Lindström theorem emerges as a geometric behaviour of coherent topoi.
David Wärn — The suspension of a set is a 1-type
Classically, the suspension of a set is a 1-type. This means that the free group on a set is also the free higher group on that set. This can be thought of as a coherence theorem for higher groups, analogous to Mac Lane's coherence theorem for monoidal categories. Until this week, this theorem was known in HoTT only assuming that the set in question has decidable equality. In this talk I present a simple general proof. It proceeds by unrecursifying Kraus-von Raumer's description of paths in a pushout, reformulating it as a sequential colimit, similar to Brunerie's version of the James construction.
Axel Ljungström — Dealing With Smash Products in HoTT
Verifying that the smash product forms a symmetric monoidal product in HoTT turns out to be rather complicated. There is no deeper reason for this: the number of coherences which need to be verified simply grows too quickly for anyone in their right mind to actually complete the naive proof by induction. In this talk, we introduce a heuristic for proving equalities of pointed maps defined over iterated smash products. With this heuristic, we significantly bound the number of coherences appearing in such proofs. In particular, this heuristic lets us prove that the smash product is symmetric monoidal in a rather straightforward manner.
Taichi Uemura — A MORE General Framework for the Semantics of Type Theory
I will present ongoing work on a better notion of type theory. In previous work (arXiv:1904.04097), I presented a general definition of type theories. In this talk, I further generalize it to a notion of multimode type theory. This new notion is worth studying at least for the following three reasons. (1) New examples include multimodal dependent type theory. (2) Normal forms and neutral terms can be part of a specification of a multimode type theory, which suggests that some general normalization theorem could be available. (3) A kind of syntax-semantics duality for type theories becomes clear.
Felix Cherubini — Synthetic Algebraic Geometry
Algebraic geometry is the study of solutions of non-linear equations using methods from geometry. The basic objects in this classical theory are called affine schemes, where, informally, an affine scheme corresponds to a solution set of polynomial equations. We use homotopy type theory together with some axioms modeled by the Zariski-topos, to have an intuitive theory, where affine schemes are solution sets of polynomial equations. To get an analogue of the most important classical tool, cohomology of schemes, we use higher types (in the homotopy theoretic sense). (project page on GitHub)
Cancelled talks
Nobody — Naturals from integers
In a setting where inductive types are not taken for granted, we say a natural number type is any type freely generated by an element and a self-map. Similarly, an integer type is any type freely generated by an element and a self-equivalence. Working in a primitive, predicative type theory without universes, we present a relatively simple construction of a natural number type from an integer type. The interest in this result comes from the fact that the loop space of the circle is an integer type, given that the circle admits large elimination. This is work of Christian Sattler and David Wärn, so ask them about it!