Coequalisers under the Lens

TL;DR

This paper investigates the properties of lenses in category theory, characterizing monic and epic lenses, studying coequalisers, and establishing an orthogonal factorisation system for lenses.

Contribution

It provides new characterizations of monic and epic lenses, analyzes coequalisers in the lens category, and introduces an orthogonal factorisation system for lenses.

Findings

Monic lenses are characterized by elementary properties of get functors.

Epic lenses are shown to be regular.

Monic and epic lenses form an orthogonal factorisation system.

Abstract

Lenses encode protocols for synchronising systems. We continue the work begun by Chollet et al. at the Applied Category Theory Adjoint School in 2020 to study the properties of the category of small categories and asymmetric delta lenses. The forgetful functor from the category of lenses to the category of functors is already known to reflect monos and epis and preserve epis; we show that it preserves monos, and give a simpler proof that it preserves epis. Together this gives a complete characterisation of the monic and epic lenses in terms of elementary properties of their get functors. Next, we initiate the study of coequalisers of lenses. We observe that not all parallel pairs of lenses have coequalisers, and that the forgetful functor from the category of lenses to the category of functors neither preserves nor reflects all coequalisers. However, some coequalisers are reflected; we study when this occurs, and then use what we learned to show that every epic lens is regular, and that discrete opfibrations have pushouts along monic lenses. Corollaries include that every monic lens is effective, every monic epic lens is an isomorphism, and the class of all epic lenses and the class of all monic lenses form an orthogonal factorisation system.