Lenses as coalgebras for a comonad
Bryce Clarke – 28 April 2021
Delta lenses were first introduced as functors equipped with a suitable choice of lifts, which implies that they are functors with additional structure. Last year I showed two ways in which this structure could be obtained, through characterising the category Lens(B) of lenses over a base as both the category of algebras for a monad on Cat / B, and as the category of lax double functors from B into sMult (the double category of split multi-valued functions). However, we also know that a lens is equal parts functor and cofunctor, so it is natural to ask: is there a nice way of characterising lenses as cofunctors with additional structure?In this talk, I will show that the forgetful functor from the category of lenses over a base to the category of cofunctors over a base, is comonadic. This result builds upon previous work of Ahman and Uustalu, who first noticed that lenses are cofunctors with additional structure, and also introduced a construction which builds a lens from a cofunctor. Through working diagrammatically, I will also demonstrate how this result may be obtained in a more general setting (than Cat), and establish a theory of lenses (and split opfibrations) in any 1-category with pullbacks and enough structure.
Back