StockholmGoteborgMeeting261104
Venue
| 11:30 - 12:00 | Room Vasa-L7, Chalmers campus, Göteborg |
| 13:10 - 17:00 | Room Analysen, EDIT building, Chalmers campus, Göteborg |
Tentative Schedule
| 11:30 - 12:00 | Hĺkon Gylterud (chair: Peter Dybjer) |
| Lunch Wijkanders | |
| 13:15 - 13:45 | Reid Barton (chair: Peter Lumsdaine) |
| 13:50 - 14:20 | Daniël Apol |
| Coffee | |
| 15:05 - 15:35 | Emily Riehl (chair: Thierry Coquand) |
| 15:40 - 16:10 | Anders Mörtberg |
| 16:15 - 17:00 | Discussion on AI and proof assistants |
| 18:00 | Dinner Andrum (map) |
Titles and Abstracts
Hĺkon Gylterud: Towards Fréchet derivatives of higher-kinded data structures - joint work with Thorsten Altenkirch and Zhili Tian
Containers model strictly positive data structures and are closed under the usual algebraic data type constructions: sums, products, fixed points and more. They are also famously differentiable: the derivative ∂F of a container F is the data structure with one of its points removed. The operator ∂ is linear and satisfies the Leibniz rule and the chain rule, which makes the analogy with analysis striking. It is, however, limited to differentiation of first-order data structures, such as lists and trees.
With the traditional container and differentiation theory as a backdrop, I aim in this talk to give intuition for differentiation of higher-kinded data structures, such as monad transformers, the fixed-point operators μ and ν, and even differentiation itself. While this is work in progress, and definitions are in flux, the analogy to the classical Fréchet derivative is clear. Furthermore, the mechanical application of the rules yields interesting decompositions of known constructions, such as the zipper construction on trees being, essentially, the Fréchet derivative of μF with respect to F.
Reid Barton: On constructive models of HoTT with standard sets
The known (cubical) models of HoTT in a constructive metatheory have the property that their h-sets are not equivalent to the sets of the metatheory, but to setoids or some even larger category. This distinction is invisible in classical mathematics but becomes relevant for building models of HoTT satisfying anticlassical axioms. It is natural to ask whether one can build a constructive model of HoTT whose h-sets agree with the ambient sets, so that the model would inherit such axioms from the metatheory. A closely related question is whether every elementary 1-topos can be realized as the 1-topos of 0-truncated objects of a higher elementary topos.
In this talk I will explain why the answer to both questions is negative. The basic obstruction is that in a model of HoTT, the construction of cohomology by means of Eilenberg–Mac Lane types gives a bound on the size of families of torsors. However, in a general elementary 1-topos there is no reason that such a bound should exist. Joint work with David Wärn.
Daniël Apol: Internal language conjectures for (pi-)tribes
We will present some current work attempting to prove internal language conjectures for certain basic flavours of homotopy type theory. More precisely, we discuss an approach to obtaining an equivalence between the oo-category of finitely complete oo-categories and a particular oo-category of tribes, and to obtaining an equivalence between the oo-category of locally cartesian closed oo-categories and a particular oo-category of pi-tribes. (At the time of writing, there is one step missing to completing these proofs, which we hope to have filled in at the time of the presentation.) Depending on results obtained in the time leading up to the talk, we discuss approaches to internal language conjectures when further type formers, like coproduct types, are added to the type theory.
We hope our approach is a bit simpler than the ones by Kapulkin-Szumilo and Cherradi, and provides a basis for future work. During the talk, we will also introduce the notion of an oo-tribe as oo-categorical analogue of a tribe (which can be compared with the oo-type theories of Nguyen-Uemura), and we hope to illustrate how this notion simplifies the comparison between tribes and oo-categories both philosophically and mathematically.
Emily Riehl: Open questions in autoformalization (of HoTT)
Frontier models have improved considerably at autoformalization over the last year, particularly targeting the computer proof assistant Lean. We will report on some experiments of a somewhat different flavor, targeting proofs in homotopy type theory formalized in Agda. We will then present some open questions, describe opportunities for collaboration, and speculate about the future.
Anders Mörtberg: A Bézout domain which is not an elementary divisor domain
A Bézout domain is an integral domain in which every finitely generated ideal is principal and an elementary divisor domain (EDD) is a domain where every matrix has a Smith normal form (SNF). A natural question, which goes back to the 1940s, is whether one can generalize the classical structure theorem for finitely presented modules over PIDs and show that every Bezout domain is an EDD? With the help of GPT-6 Astra Christian Hägg and I recently answered this negatively by finding a counterexample in the form of a Bezout domain in which an explicit 2x2 matrix does not have a SNF. We also have a Lean autoformalization of the result and Thierry recently had Claude produce a constructive version of the proof and formalization. In the talk I will introduce the problem, discuss how we found the counterexample and what we currently understand about it.
More generally this talk will be about a concrete instance of the recent situation where an AI has found a proof which we humans don't understand (yet?).