The Grothendieck construction for delta lenses
Bryce Clarke
TL;DR
The paper establishes a Grothendieck-style construction for delta lenses by proving a canonical correspondence with lax double functors into the double category of split multivalued functions $\mathrm{SMult}$. It shows an overarching equivalence $\mathcal{L}ens \simeq \mathrm{Idx}(\mathcal{C}at, \mathrm{SMult})$, built via diagrammatic delta lenses and the category of elements, and then connects these results to a network of double-categorical formalisms including $\mathrm{GlobCone}(\mathcal{Dbl},K_*)$, spans, and profunctor-like structures. The introduction of $\mathrm{SMult}$ comes with both 1-dimensional and 2-dimensional universal properties, enabling concrete characterizations of delta lenses, split opfibrations, and indexed split multivalued functions, along with a suite of applications: adjunctions with discrete opfibrations, descriptions as bimodules, pullbacks/pushforwards, and factorisations through sub-double categories. Collectively, these results provide a robust double-categorical framework for delta lenses, yielding representation theorems, adjunctions, and structural insights that integrate state-based lens theory with Grothendieck-style constructions and diagrammatic calculus.
Abstract
Delta lenses are functors equipped with a functorial choice of lifts, generalising the notion of split opfibration. In this paper, we introduce a Grothendieck construction (or category of elements) for delta lenses, thus demonstrating a correspondence between delta lenses and certain lax double functors into the double category of sets, functions, and split multivalued functions. We show that the double category of split multivalued functions admits a universal property as a certain kind of limit, and inherits many nice properties from the double category of spans. Applications of this construction to the theory of delta lenses are explored in detail.