[msp-interest] [MSP101] Jules Hedges: We solved dependent optics! (LT209, 3pm Mon 3-Feb)

[Dilsat Yuksel]

Hi all,

On Monday, the MSP101 talk will be given by Jules Hedges (MSP, Cybercat Inst.). See the details of the talk below.

Best,
Dilsat

**********************************************************************

Date: Monday, 03 February at 15:00

Room: LT209, Livingstone Tower

Zoom link: https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1

Speaker: Jules Hedges

Title: We solved dependent optics!

Abstract: There are two major generalisations of lenses. First there are optics, which require almost nothing of their base category and give you something in return. And then there are dependent lenses (aka container morphisms, aka natural transformations of polynomials), which require a lot of their base category but give you even more in return. One day several years ago I innocently twote the question of how to unify these two constructions, which is motivated for mathematical, computational and sociological reasons. The problem ended up occupying us (joint work with Dylan Braithwaite, Matteo Capucci, Bruno Gavranović, Eigil Rischel and André Videla) for several years, and its difficulty became a meme.

I will explain the answer that finally satisfied us. This involves first constructing a category of "dependent adaptors" and then freely adjoining a particular family of monoidal costates using a technique we call "weighted coparametrisation" that we reinvented. The definition began life as a prototype in Idris using QTT features, and was then translated back into category theory using what might or might not be a novel semantics of polymorphic dependent type theory.

**********************************************************************

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20250130/b60a2583/attachment.html