Proxy pullbacks in the category of lenses
Matthew di Meglio – 15 December 2021
The category of (asymmetric delta) lenses has several surprisingly-nice categorical properties—these have been discussed in several other Australian Category Seminar talks by Clarke and myself throughout 2021. An important construction for the proofs of many of these properties is Johnson and Rosebrugh's “pullback” of lenses, which we will call the proxy pullback of lenses, adopting this new terminology from Bumpus and Kocsis. 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.
Back