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.
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 [1], also known as state-based lenses [2], have been understood as both algebras for a monad [3] and coalgebras for a comonad [4, 5]. A generalisation of state-based lenses called category lenses [6] were also introduced as algebras for a monad, based on classical work in 2-category theory on split opfibrations [ 7]. Another kind of lens between categories called a delta lens [8] was shown to be a certain algebra for a semi-monad [9], 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 [2] as morphisms of directed containers [10], which are equivalent to certain morphisms called cofunctors between categories [11]. 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 [12] 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 [13], building upon an earlier characterisation of cofunctors as spans [14]. This diagrammatic approach is utilised throughout this paper, and leads to another simple characterisation of delta lenses (Proposition 6).
This section provides an informal overview of the paper, together with further commentary on the background, and references to related work. The goal is to provide a conceptual understanding of the results; later sections will be dedicated to the formal mathematics.
Section 2 contains the mathematical background required for the main results, which are presented in Section 3. Consequences of the main result and concluding remarks are in Section 4.
Throughout the paper we make the assumption that a system, whatever that may be, can be understood as a category. The objects of this category are the states of the system, while the morphisms are the transitions (or deltas) between system states.
Delta lenses were introduced in [8, Definition 4] to model bidirectional transformations between systems when they are understood as categories. The Get of a delta lens is a functor : → from the source category to the view category , while the Put is a certain kind of function (that this paper calls a lifting operation) satisfying axioms analogous to the classical lens laws. A slightly modified definition of delta lens appeared in [ 9, Definition 1], however this definition still seemed to be ad hoc, and made it dificult to prove deep results without checking many details.
The definition of delta lens (Definition 4) given in this paper is based on a diagrammatic characterisation which first appeared in [ 13, Corollary 20], by representing the Put in terms of bijective-on-objects functors (Definition 1) and discrete opfibrations (Definition 2). This diagrammatic approach provides a natural framework for studying delta lenses using category theory, and has the benefit of allowing for very simple (albeit more abstract) proofs. This approach will be utilised throughout this paper, although in many places we will also include explicit descriptions of constructions using the traditional definition of a delta lens.
A key idea presented in [2, 13] is that the Get and Put of a delta lens can be separated into functors and cofunctors (Definition 3), respectively. Intuitively, a cofunctor can be understood as a delta lens without any information on how the Get acts on morphisms; it is the minimum amount of structure needed to specify a Put operation between categories. It was shown in the paper [2] that delta lenses are cofunctors with additional structure. In this paper, we aim to show that said structure arises coalgebraically via a comonad.
Both delta lenses and cofunctors are predominantly understood and studied as morphisms between categories, however to prove that delta lenses are cofunctors equipped with coalgebraic structure, it is necessary for them to be understood as objects. Therefore this paper introduces a new category Cof(), whose objects are cofunctors into a fixed category (Definition 5). The category Lens(), whose objects are delta lenses into a fixed category , was previously studied in [15, 16]. Surprisingly, we show that the category Lens() can be defined (Definition 7) as projection from a slice category. the slice category Cof()/1. Not only does this provide a new characterisation of delta lenses in term of cofunctors (Proposition 6), but also provides the insight that the canonical forgetful functor : Lens() → Cof(), which takes a delta lens to its underlying Put cofunctor, is a
Finally, proving that delta lenses are coalgebras for a comonad on Cof() amounts to showing that the forgetful functor : Lens() → Cof() is comonadic (Theorem 9). A necessary condition is that has a right adjoint (Lemma 8), which constructs the cofree delta lens from each cofunctor in Cof(). This construction first appeared explicitly in [ 12, Section 3.2], however it was not obviously a right adjoint — or even a functor — and it was disconnected from the context of cofunctors and delta lenses. Both Lemma 8 and Theorem 9 admit straightforward proofs, with the benefit of the diagrammatic approach to cofunctors and delta lenses.
This section outlines some of the notation and conventions used in the paper. Given a category , its underlying set (or discrete category) of objects is denoted 0. Given a functor : → , its underlying object assignment is denoted 0 : 0 → 0. Similarly, a cofunctor : ↛ will have an underlying object assignment 0 : 0 → 0. Thus the orientation of a cofunctor agrees with the orientation of its underlying object assignment (this convention is chosen to agree with the orientation of delta lenses, however this choice is not uniform in the literature on cofunctors). The operation cod sends each morphism to its codomain or target object.
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 Cof() whose objects are cofunctors (Definition 5), and the characterisation of delta lenses as certain morphisms therein (Proposition 6).
0 : 0 → 0 is a bijection.
A functor : → is a discrete opfibration if for all pairs,
A functor : → is bijective-on-objects if its underlying object assignment there exists a unique morphism : → ′ in such that = .
A cofunctor : ↛ between categories is a span of functors,
( ∈ , : → ∈ )
where is a bijective-on-objects functor and is a discrete opfibration.
(
We can also describe a delta lens (, ) : ⇌
as consisting of a functor : →
morphism (, ) : → ′ in , such that the following axioms are satisfied:
together with a lifting operation , which assigns each pair ( ∈ , : → ∈ ) to a
(
(
Every delta lens (, ) : ⇌
has an underlying functor : → and an underlying cofunctor : ↛ , and their corresponding underlying object assignments are equal; that is,
For each category , there is a category Cof() of cofunctors over the base whose objects are cofunctors with codomain , and whose morphisms are given by commutative diagrams of functors of the form: (, ) : → ′ in , such that the following axioms are satisfied:
Alternatively, a cofunctor : ↛ consists of a function 0 : 0 → 0, together with
a lifting operation , which assigns each pair ( ∈ , : 0 → ∈ ) to a morphism
(
functors,
A delta lens (, ) : ⇌
between categories is a commutative diagram of
Equivalently, a morphism in Cof() from a cofunctor : ↛ to a cofunctor : ↛ this data. Intuitively, if and are understood as source categories with a fixed consists of a functor ℎ : → such that 0ℎ = 0 for all ∈ , and ℎ (, ) = (ℎ, ) for all pairs ( ∈ , : 0 → ∈ ). The functor ℎ : → is then uniquely induced from view category , then the morphisms in Cof() are functors between the source categories which preserve the chosen lifts, given by the corresponding cofunctors, from the view category.
ℎ ℎ
(
We can unpack (
For each category , we define the category of delta lenses over the base to be the slice category Lens() := Cof() / 1, where 1 is the trivial cofunctor on .
By Proposition 6, the objects of Lens() are delta lenses with codomain , represented as a
morphism into the trivial cofunctor as shown in (
Proof. Consider the morphism in Cof() given by the commutative diagram of functors:
(
1 1 In other words, the only additional requirement on a morphism ℎ : → between delta lenses over , compared to a morphism between cofunctors over , is that ∘ ℎ = . This is opposed to just requiring 0ℎ = 0 on objects (where recall for delta lenses, the underlying object assignments for the functor and cofunctor are equal, that is, 0 = 0 and 0 = 0).
There is a canonical forgetful functor, : Lens() →−
Cof() which assigns every delta lens to its underlying cofunctor. This forgetful functor is the focus of the main result in the following section.
̂︀0 ∘
̂︀0 ∘ ⌟ ̂︀0 ⌟ ̂︀0
construct the following pullback in Cat: (− ̂︀ ) : Set → Cat which takes each set to the codiscrete category ̂︀ .
While not every cofunctor may be given the structure of a delta lens, Ahman and Uustalu [12] developed a method which constructs a delta lens from any cofunctor. To understand their construction, first recall that the underlying objects functor (− )0 : Cat → Set has a right adjoint
Given a cofunctor : ↛ with underlying object assignment 0 : 0 → 0, we may
Here : → ̂︀0 is the component of the unit for the adjunction at , and ̂︀0 ∘ the
component of the unit at followed by image of 0 under the right adjoint. Using the universal
property of the pullback, we have the following:
Since is bijective-on-objects, the projection functor is also bijective-on-objects which,
together with the functor , implies that ⟨, ⟩ : → is bijective-on-objects, due to the
properties of bijections at the level of objects. Thus, the upper right triangle in (
.
The category has the same objects as , but morphisms → ′ in are given by pairs of the form ( : → ′ ∈ , : 0 → 0′ ∈ ). The functor : → projects to the second arrow in this pair. The lifting operation which makes this functor into a delta lens morphism : 0 → ∈ to the morphism (︀ (, ) : → ′, : 0 → ︀) in . is induced by the lifting operation of the original cofunctor; it takes an object ∈ and a
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. ment: Lemma 8. The forgetful functor : Lens() → Cof() has a right adjoint.
Proof. Using the construction in (
1 1 1 ℎ ℎ
=
Given a delta lens (, ) : ⇌ the component of the unit is given by: detailed checks that the triangle identities hold.
We describe the components of the unit and counit for the adjunction ⊣ and omit the
Given a cofunctor : ↛ the component of the counit is given by:
(
Proof. By Lemma 8, the functor has a right adjoint . To prove that is comonadic, it remains to show that the category of coalgebras for the induced comonad on Cof() is equivalent
Given a cofunctor : ↛ , a coalgebra structure map is given by a morphism in Cof() to Lens(). of the form: functor such that ∘ (, ) : ⇌
.
However compatibility with the counit forces ℎ = 1 and ℎ = ⟨1, ⟩, where : → is a = . Compatibility with the comultiplication doesn’t add any further conditions. Therefore, a coalgebra for the comonad on Cof() is equivalent to a delta lens
This theorem establishes the result stated in the title of the paper, that delta lenses (
In this paper, the category Lens() of delta lenses over the base was characterised as the category of coalgebras for a comonad on the category Cof() of cofunctors over the base . 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 [2] characterisation of delta lenses is coalgebraic, and that their construction of a delta lens from cofunctor in the paper [12] 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 [ 13], has led to concise proofs of these results, and ofers 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 : Lens() → Cof() creates all colimits which exist in Cof(). Thus we can take the coproduct of a pair of cofunctors in Cof(), and automatically know how to construct the coproduct of the corresponding delta lenses in Lens().
Another consequence from the unit (10) of the adjunction between Cof() and Lens() 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 with a transition in the view category via the functor part : → of the delta lens, : → ′ ∈ →−↦
( : → ′ ∈ , : → ′ ∈ ) then consider the update propagation determined by the cofunctor part : ↛ 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, 18], 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 [2], 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 [4, 5]. 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 Set being a cartesian closed category, and arises from the adjunction (− ) × ⊣ [, − ], whereas the results in this paper arise from a diferent 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 Lens() is comonadic over other categories (such as Cat as was suggested by an anonymous reviewer), or if split opfibrations (also known as c-lenses [ 6]) are also comonadic over Cof(). In recent work by the current author, it has been demonstrated that delta lenses arise as algebras for a monad on Cat/, providing a dual to the main result of this paper and strengthening the previous work of Johnson and Rosebrugh [9]. Finally, given the importance of the category Lens() in the study of symmetric lenses [15, 16], it is also hoped that the coalgebraic perspective provides new insights into this area, and this will be the subject of further investigation.
The author would like to thank Michael Johnson for his feedback on this work, the anonymous reviewers of this paper for their helpful comments, and the audience of the Bx2021 workshop for their insightful questions. The author also thanks Eli Hazel and Giacomo Tendas for their suggestions which improved the final version of this paper. The author is grateful for the support of the Australian Government Research Training Program Scholarship. [10] D. Ahman, J. Chapman, T. Uustalu, When is a container a comonad?, Logical Methods in
Computer Science 10 (2014) 1–48. doi:10.2168/LMCS-10(3:14)2014. [11] M. Aguiar, Internal Categories and Quantum Groups, Ph.D. thesis, Cornell University, 1997. [12] D. Ahman, T. Uustalu, Directed containers as categories, in: Proceedings 6th Workshop on Mathematically Structured Functional Programming, volume 207 of Electronic Proceedings in Theoretical Computer Science, 2016, pp. 89–98. doi:10.4204/EPTCS.207.5. [13] B. Clarke, Internal lenses as functors and cofunctors, in: Applied Category Theory 2019, volume 323 of Electronic Proceedings in Theoretical Computer Science, 2020, pp. 183–195. doi:10.4204/EPTCS.323.13. [14] P. J. Higgins, K. C. H. Mackenzie, Duality for base-changing morphisms of vector bundles, modules, Lie algebroids and Poisson structures, Mathematical Proceedings of the Cambridge Philosophical Society 114 (1993) 471–488. doi:10.1017/S0305004100071760. [15] M. Johnson, R. Rosebrugh, Universal updates for symmetric lenses, in: Proceedings of the 6th International Workshop on Bidirectional Transformations, volume 1827 of CEUR Workshop Proceedings, 2017, pp. 39–53. URL: http://ceur-ws.org/Vol-1827/paper8.pdf. [16] B. Clarke, A diagrammatic approach to symmetric lenses, in: Applied Category Theory Conference 2020, volume 333 of Electronic Proceedings in Theoretical Computer Science, 2021, pp. 79–91. doi:10.4204/EPTCS.333.6. [17] H. Pacheco, Z. Hu, S. Fischer, Monadic combinators for putback style bidirectional programming, in: Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation, volume 333 of PEPM ’14, 2014, pp. 39–50. doi:10.1145/2543728. 2543737. [18] S. Fischer, Z. Hu, H. Pacheco, The essence of bidirectional programming, Science China Information Sciences 58 (2015) 1–21. doi:10.1007/s11432-015-5316-8.