The category of asymmetric lenses and its proxy pullbacks

We study the categorical properties of the category of small categories and asymmetric delta lenses, continuing the work begun by Chollet et al. at the Applied Category Theory Adjoint School 2020. We give complete elementary characterisations of the monic and epic lenses, confirming several of Chollet et al.’s conjectures. We also initiate the study of lens co-equalisers, ultimately showing that every epic lens is regular, and that discrete opfibrations have pushouts along monic lenses. An important construction for proving many of these results 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. We also prove that the proxy pullback has several pullback-like properties, including an analogue of the well-known pullback pasting lemma. 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.