Universal Properties of Lens Proxy Pullbacks

TL;DR

This paper explores the categorical properties of small categories and asymmetric delta lenses, introducing a new perspective on the proxy pullback of lenses through compatibility and characterizing conditions for when it forms a true pullback.

Contribution

It provides a novel treatment of the proxy pullback using compatibility and introduces concepts like sync-minimal and independent lens spans for better characterization.

Findings

Proxy pullback is not always a true pullback.

Compatibility is a key notion for understanding proxy pullbacks.

Characterization of when a lens span has a comparison lens to a proxy pullback.

Abstract

A comprehensive account of the categorical properties of the category of small categories and asymmetric delta lenses is given in the recent works of Chollet et al. and Di Meglio. An important construction for proving many of these properties is Johnson and Rosebrugh's "pullback" of lenses, which we call the proxy pullback of lenses. We give a new treatment of the proxy pullback in terms of compatibility, a stronger notion of commutativity for squares of lenses. The proxy pullback is sometimes, but not always, a real pullback. Using new notions of sync-minimal and independent lens spans, we characterise when a lens span that forms a commuting square with a lens cospan has a comparison lens to a proxy pullback of the cospan.