StockholmGoteborgMeeting210428
Stockholm–Göteborg meeting on Wednesday, 28 April 2021 online
Program
| Time | Speaker | Title |
|---|---|---|
| 14:00–15:00 | Evan Cavallo | Fitch-style Modalities and Parametric Adjoints |
| fika | ||
| 15:30–16:15 | Axel Ljungström | Cohomology Computations in Cubical Agda |
| 16:15–17:00 | Nils Anders Danielsson | Higher lenses |
| social gathering |
Abstracts
Evan Cavallo — Fitch-style Modalities and Parametric Adjoints
Modalities appear everywhere in mathematics, but can prove difficult to represent in type theory when they interact non-trivially with the ambient context. Birkedal et al. introduce dependent right adjoints as a class of modalities that can be represented in type theory; the right adjoint gives the modal type former, while the left adjoint appears in its rules as an operator on the context. However, the elimination rule for a dependent right adjoint is problematic: its stability under substitution is delicate and prevents the effective use of the theory as an internal language, and it is difficult to generalize to theories in which multiple modalities interact. I'll talk about joint work with Daniel Gratzer, G.A. Kavvos, Adrien Guatto, and Lars Birkedal in which we identify a further condition—that the left adjoint is also a parametric right adjoint—under which these problems can be resolved. We find that this condition is commonly satisfied, in particular in the standard models of guarded and internally parametric type theory.
Axel Ljungström — Cohomology Computations in Cubical Agda
I will present some recent work on integer cohomology computations in Cubical Agda (j.w.w. Guillaume Brunerie and Anders Mörtberg). Our cohomology theory has a relatively direct definition and allows for fast computations in some cases. However, many computations are still slow/infeasible already for cohomology in dimension two. The functions involved in these computations are often similar to those appearing in the definition of the "Brunerie number". This allows us to produce a large family of similar numbers of varying complexity. Our hope is that understanding the bottlenecks for the computations of these numbers can help shed some light on why more complicated computations, like that of the Brunerie number, currently seem infeasible in Cubical Agda.
Nils Anders Danielsson — Higher lenses
Lenses are commonly used in functional programming languages to compositionally access and update data in nested data structures. One variant of such lenses involves two functions—a getter and a setter—that should satisfy three lens laws. If the laws are included in the representation, then we end up with something that is not very well-behaved in a higher setting. I will present higher lenses, which are more well-behaved.
The presentation is based on work done together with Paolo Capriotti and Andrea Vezzosi.