Delta lenses as coalgebras for a comonad

TL;DR

This paper demonstrates that delta lenses can be characterized as coalgebras for a specific comonad, providing new insights into their structure and relationship with cofunctors.

Contribution

It establishes that delta lenses are coalgebras for a comonad, expanding the theoretical understanding of their categorical properties.

Findings

Delta lenses are coalgebras for a comonad.

The forgetful functor from delta lenses to cofunctors is comonadic.

Clarifies the relationship between delta lenses and cofunctors.

Abstract

Delta lenses are a kind of morphism between categories which are used to model bidirectional transformations between systems. Classical state-based lenses, also known as very well-behaved lenses, are both algebras for a monad and coalgebras for a comonad. Delta lenses generalise state-based lenses, and while delta lenses have been characterised as certain algebras for a semi-monad, it is natural to ask if they also arise as coalgebras. This short paper establishes that delta lenses are coalgebras for a comonad, through showing that the forgetful functor from the category of delta lenses over a base, to the category of cofunctors over a base, is comonadic. The proof utilises a diagrammatic approach to delta lenses, and clarifies several results in the literature concerning the relationship between delta lenses and cofunctors. Interestingly, while this work does not generalise the corresponding result for state-based lenses, it does provide new avenues for exploring lenses as coalgebras.