The Grothendieck construction for delta lenses

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.

arXiv comment41 pages