The category of lenses is regular-ish

Matthew di Meglio – 11 August 2021

The category Lens of small categories and asymmetric delta lenses has surprisingly nice categorical properties. A recent study of the monos and epis in Lens has revealed that Lens has properties similar to those of a regular category, except with the notions of pullback and kernel pair replaced by their canonical proxies in Lens. Some of these properties include that

* the proxy effective, regular, strong and extremal epics in Lens coincide (all epic lenses coequalise their proxy kernel pair and so are proxy effective); * the (regular) epis and monos in Lens form an orthogonal factorisation system; and, * image factorisations in Lens are proxy pullback stable.