The double category of generalised lenses

Bryce Clarke – 22 September 2021

Delta lenses are functors equipped with additional structure specifying a suitable choice of lifts. Typically delta lenses are understood as morphisms between categories, consisiting of a compatible functor and cofunctor pair. However, delta lenses also arise as objects in a category of algebras for a monad. These two approaches can be unified via a double category whose objects are categories, whose horizontal morphisms are functors, and whose vertical morphisms are delta lenses. The goal of this talk is to explore how this provides a natural context for considering generalisations of lenses.

I will first define generalised lenses as morphisms with additional structure, working in a category equipped with an idempotent comonad and an orthogonal factorisation system (OFS); working in Cat together with the idempotent comonad for discrete categories and the comprehensive factorisation system yields the case of delta lenses. I will then show that generalised lenses retain a notion of ``suitable choice of lifts'', through showing that they arise as the right class of an algebraic weak factorisation system (AWFS). This generalises a previous result where delta lenses were characterised as algebras for a monad, and also provides a way of constructing an AWFS from an OFS. Finally, as a corollary, I will show that the double category of generalised lenses is a monadic right-connected double category corresponding to the AWFS.