Constructing lenses in double categories

Abstract: Lenses are a family of mathematical structures used to model bidirectional transformations between systems. A common feature among all kinds of lenses is that they consist of a "forwards" component and a "backwards" component. A double category is a 2-dimensional categorical structure consisting of objects, two types of morphism (horizontal and vertical), and cells between them. A natural question arises: what if the forwards and backwards components of a lens were the horizontal and vertical morphisms in a double category?

In this talk, I advocate for a double categorical approach to lenses, and demonstrate how many examples of lenses, particularly those satisfying "lens laws", may be built from the horizontal and vertical morphisms in a double category. A general process for constructing lenses inside any double category, called the "right-connected completion", is introduced and is shown to satisfy a universal property. Finally, we explore how many questions and properties of lenses may be understood in the setting of double categories.

category theory

Audience: researchers in the topic

( video )

Intercats: Seminar on Categorical Interaction