Delta lenses as coalgebras for a comonad

The goal of understanding various kinds of lenses as mathematical structures has been an ongoing program in the study of bidirectional transformations. For example, very well-behaved lenses [9], also known as state-based lenses [4], have been understood as both algebras for a monad [14] and coalgebras for a comonad [16, 10]. A generalisation of state-based lenses called category lenses [15] were also introduced as algebras for a monad, based on classical work in $2$-category theory on split opfibrations [18]. Another kind of lens between categories called a delta lens [7] was shown to be a certain algebra for a semi-monad [12], however it remained open as to whether delta lenses could also be characterised as (co)algebras for a (co)monad.

The purpose of this short paper is to characterise delta lenses as coalgebras for a comonad (Theorem 9). The proof of this simple result builds upon and clarifies several recent advances in the theory of delta lenses.

In 2017, Ahman and Uustalu introduced update-update lenses [4] as morphisms of directed containers [2], which are equivalent to certain morphisms called cofunctors between categories [1]. In the same paper, they show explicitly how, using the notation of directed containers, delta lenses may be understood as cofunctors with additional structure.

In earlier work [3] from 2016, Ahman and Uustalu also provide a construction on morphisms of directed containers which yields a split pre-opcleavage for a functor; in other words, they show how cofunctors may be turned into delta lenses. We show that this construction is actually a right adjoint to the forgetful functor from delta lenses to cofunctors (Lemma 8), and that the coalgebras for the comonad generated from this adjunction are delta lenses (Theorem 9).

In 2020, a diagrammatic characterisation of delta lenses was introduced by the current author [5], building upon an earlier characterisation of cofunctors as spans [11]. This diagrammatic approach is utilised throughout this paper, and leads to another simple characterisation of delta lenses (Proposition 6).

We first recall two special classes of functors, which we will use as the building blocks for defining cofunctors and delta lenses. New contributions in this section include the category $\mathsf{Cof}(B)$ whose objects are cofunctors (Definition 5), and the characterisation of delta lenses as certain morphisms therein (Proposition 6).

Alternatively, a cofunctor $\varphi\colon A\nrightarrow B$ consists of a function $\varphi_{0}\colon A_{0}\rightarrow B_{0}$, together with a lifting operation $\varphi$, which assigns each pair $(a\in A,\,u\colon\varphi_{0}a\rightarrow b\in B)$ to a morphism $\varphi(a,u)\colon a\rightarrow~{}a^{\prime}$ in $A$, such that the following axioms are satisfied:

1. (1)

   $\varphi_{0}\operatorname{cod}\big{(}\varphi(a,u)\big{)}=\operatorname{cod}(u)$;

2. (2)

   $\varphi(a,1_{\varphi_{0}a})=1_{a}$;

3. (3)

   $\varphi(a,v\circ u)=\varphi(a^{\prime},v)\circ\varphi(a,u)$, where $a^{\prime}=\operatorname{cod}\big{(}\varphi(a,u)\big{)}$.

We can also describe a delta lens $(f,\varphi)\colon A\rightleftharpoons B$ as consisting of a functor $f\colon A\rightarrow B$ together with a lifting operation $\varphi$, which assigns each pair $(a\in A,\,u\colon fa\rightarrow b\in B)$ to a morphism $\varphi(a,u)\colon a\rightarrow a^{\prime}$ in $A$, such that the following axioms are satisfied:

1. (1)

   $f\varphi(a,u)=u$;

2. (2)

   $\varphi(a,1_{fa})=1_{a}$;

3. (3)

   $\varphi(a,v\circ u)=\varphi(a^{\prime},v)\circ\varphi(a,u)$, where $a^{\prime}=\operatorname{cod}\big{(}\varphi(a,u)\big{)}$.

Every delta lens $(f,\varphi)\colon A\rightleftharpoons B$ has an underlying functor $f\colon A\rightarrow B$ and an underlying cofunctor $\varphi\colon A\nrightarrow B$, and their corresponding underlying object assignments are equal; that is, $f_{0}=\varphi_{0}$.

Equivalently, a morphism in $\mathsf{Cof}(B)$ from a cofunctor $\varphi\colon A\nrightarrow B$ to a cofunctor $\gamma\colon C\nrightarrow B$ consists of a functor $h\colon A\rightarrow C$ such that $\gamma_{0}ha=\varphi_{0}a$ for all $a\in A$, and $h\varphi(a,u)=\gamma(ha,u)$ for all pairs $(a\in A,\,u\colon\varphi_{0}a\rightarrow b\in B)$. The functor $\overline{h}\colon X\rightarrow Y$ is then uniquely induced from this data. Intuitively, if $A$ and $C$ are understood as source categories with a fixed view category $B$, then the morphisms in $\mathsf{Cof}(B)$ are functors between the source categories which preserve the chosen lifts, given by the corresponding cofunctors, from the view category.

We can unpack (4) using the explicit characterisation of morphisms in $\mathsf{Cof}(B)$ to obtain the precise difference between cofunctors and delta lenses, in terms of objects and morphisms. Namely, the diagram (4) states that a delta lens corresponds to a cofunctor $\varphi\colon A\nrightarrow B$ together with a functor $f\colon A\rightarrow B$ such that $fa=\varphi_{0}a$ for all $a\in A$, and $f\varphi(a,u)=u$ for all pairs $(a\in A,\,u\colon fa\rightarrow b\in B)$.

By Proposition 6, the objects of $\mathsf{Lens}(B)$ are delta lenses with codomain $B$, represented as a morphism into the trivial cofunctor as shown in (4). The morphisms in $\mathsf{Lens}(B)$ are given by morphisms (3) in $\mathsf{Cof}(B)$ such that the following pasting condition holds:

In other words, the only additional requirement on a morphism $h\colon A\rightarrow C$ between delta lenses over $B$, compared to a morphism between cofunctors over $B$, is that $g\circ h=f$. This is opposed to just requiring $\gamma_{0}ha=\varphi_{0}a$ on objects (where recall for delta lenses, the underlying object assignments for the functor and cofunctor are equal, that is, $g_{0}=\gamma_{0}$ and $f_{0}=\varphi_{0}$).

There is a canonical forgetful functor,

which assigns every delta lens to its underlying cofunctor. This forgetful functor is the focus of the main result in the following section.

While not every cofunctor may be given the structure of a delta lens, Ahman and Uustalu [3] developed a method which constructs a delta lens from any cofunctor. To understand their construction, first recall that the underlying objects functor $(-)_{0}\colon\mathsf{Cat}\rightarrow\mathsf{Set}$ has a right adjoint $(\widehat{-})\colon\mathsf{Set}\rightarrow\mathsf{Cat}$ which takes each set $X$ to the codiscrete category $\widehat{X}$.

Given a cofunctor $\varphi\colon A\nrightarrow B$ with underlying object assignment $\varphi_{0}\colon A_{0}\rightarrow B_{0}$, we may construct the following pullback in $\mathsf{Cat}$:

Here $\eta_{B}\colon B\rightarrow\widehat{B}_{0}$ is the component of the unit for the adjunction at $B$, and $\widehat{\varphi}_{0}\circ\eta_{A}$ the component of the unit at $A$ followed by image of $\varphi_{0}$ under the right adjoint. Using the universal property of the pullback, we have the following:

Since $\eta_{B}$ is bijective-on-objects, the projection functor $\pi_{A}$ is also bijective-on-objects which, together with the functor $\varphi$, implies that $\langle\varphi,\overline{\varphi}\rangle\colon X\rightarrow P$ is bijective-on-objects, due to the properties of bijections at the level of objects. Thus, the upper right triangle in (7) defines a delta lens $P\rightleftharpoons B$.

The category $P$ has the same objects as $A$, but morphisms $a\rightarrow a^{\prime}$ in $P$ are given by pairs of the form $(w\colon a\rightarrow a^{\prime}\in A,u\colon\varphi_{0}a\rightarrow\varphi_{0}a^{\prime}\in B)$. The functor $\pi_{B}\colon P\rightarrow B$ projects to the second arrow in this pair. The lifting operation which makes this functor into a delta lens is induced by the lifting operation of the original cofunctor; it takes an object $a\in P$ and a morphism $u\colon\varphi_{0}a\rightarrow b\in B$ to the morphism $\big{(}\varphi(a,u)\colon a\rightarrow a^{\prime},u\colon\varphi_{0}a\rightarrow b\big{)}$ in $P$.

We now show that this construction due to Ahman and Uustalu is universal, in the sense that it provides a right adjoint to the functor taking a delta lens to its underlying cofunctor.

This theorem establishes the result stated in the title of the paper, that delta lenses (2) are coalgebras (11) for a comonad.

In this paper, the category $\mathsf{Lens}(B)$ of delta lenses over the base $B$ was characterised as the category of coalgebras for a comonad on the category $\mathsf{Cof}(B)$ of cofunctors over the base $B$. This brings together recent results in the study of delta lenses and cofunctors. In particular, we have shown that the extra structure on cofunctors given in Ahman and Uustalu’s [4] characterisation of delta lenses is coalgebraic, and that their construction of a delta lens from cofunctor in the paper [3] is precisely the cofree delta lens on a cofunctor. Throughout we have also shown how the abstract diagrammatic approach to delta lenses, first introduced in [5], has led to concise proofs of these results, and offers a clear perspective on the relationship between these ideas.

Aside from clarification and development of theory, the results presented in this paper have several other mathematical consequences. For example, the functor $L\colon\mathsf{Lens}(B)\rightarrow\mathsf{Cof}(B)$ creates all colimits which exist in $\mathsf{Cof}(B)$. Thus we can take the coproduct of a pair of cofunctors in $\mathsf{Cof}(B)$, and automatically know how to construct the coproduct of the corresponding delta lenses in $\mathsf{Lens}(B)$.

Another consequence from the unit (10) of the adjunction between $\mathsf{Cof}(B)$ and $\mathsf{Lens}(B)$ is that every delta lens factorises into a bijective-on-objects functor followed by a cofree lens. Intuitively, this allows us to first pair every transition in the source category $A$ with a transition in the view category $B$ via the functor part $f\colon A\rightarrow B$ of the delta lens,

then consider the update propagation determined by the cofunctor part $\varphi\colon A\nrightarrow B$ of the delta lens. The cofree delta lens on a cofunctor behaves much like an analogue of constant complement state-based lenses, except that the complement is with respect to morphisms rather than objects.

While the main contributions of this paper are mathematical, it is hoped that these results also prompt new ways of understanding delta lenses. For example, previously state-based lenses have been considered from a “Put-based” perspective [17, 8], however this approach could also be adapted to the setting of delta lenses. Rather than starting with a Get functor between systems and then asking how we might construct a delta lens, we might instead start with a Put cofunctor and then ask for ways in which this can be given the structure of a delta lens. This shift of focus is subtle but important, especially in the context of the ideas in [4], as it is arguably the Put structure (rather than the Get structure) which is central to the study of bidirectional transformations and lenses.

On an separate note, it is worth remarking on the similarity between the main result of this paper and the classical result stating that very well-behaved lenses are coalgebras for a comonad [16, 10]. Despite the clear analogy between them, and the inspiration that this paper derives from the classical result, it seems that they are unrelated at a mathematical level. The classical result relies on $\mathsf{Set}$ being a cartesian closed category, and arises from the adjunction $(-)\times B\dashv[B,-]$, whereas the results in this paper arise from a different adjunction, and don’t require any aspect of cartesian closure.

There are many questions to be explored in future work. For instance, it is natural to ask if $\mathsf{Lens}(B)$ is comonadic over other categories (such as $\mathsf{Cat}$ as was suggested by an anonymous reviewer), or if split opfibrations (also known as c-lenses [15]) are also comonadic over $\mathsf{Cof}(B)$. In recent work by the current author, it has been demonstrated that delta lenses arise as algebras for a monad on $\mathsf{Cat}/B$, providing a dual to the main result of this paper and strengthening the previous work of Johnson and Rosebrugh [12]. Finally, given the importance of the category $\mathsf{Lens}(B)$ in the study of symmetric lenses [13, 6], it is also hoped that the coalgebraic perspective provides new insights into this area, and this will be the subject of further investigation.