Till innehåll på sidan

Joint Stockholm–Göteborg Type Theory Seminar

Tid: On 2021-04-28 kl 14.00 - 18.00

Plats: Zoom, meeting ID: 610 2070 5696

Exportera till kalender

Full schedule

14:00 Evan Cavallo, Stockholm — Fitch-style Modalities and Parametric Adjoints
15:00 Coffee break
15:30 Axel Ljungström, Stockholm — Cohomology Computations in Cubical Agda
16:15 Nils Anders Danielsson, Göteborg — Higher lenses
17:00 Social gathering

(Social breaks will use Gather, to be distributed nearer the time.)

Abstracts

Title: Fitch-style Modalities and Parametric Adjoints
Speaker: Evan Cavallo
Abstract: 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.

Title: Cohomology Computations in Cubical Agda
Speaker: Axel Ljungström
Abstract: 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.

Title: Higher lenses
Speaker: Nils Anders Danielsson
Abstract: 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.