nLab delta lens

Idea

A delta lens (or d-lens) is a functor with additional structure specifying a suitable choice of lifts. Delta lenses can be understood in a number of ways:

• A morphism between categories which is both functor and cofunctor;

• A generalization of split Grothendieck opfibrations where the chosen lifts need not be opcartesian morphisms;

• A categorification of classical lenses between sets.

Definition

A delta lens $(f, \varphi) : A \to B$ from a category $A$ to a category $B$ consists of a functor $f : A \to B$ together with a lifting operation sending each pair $(a \in A, u : f a \to b \in B)$ to a morphism $\varphi(a, u) : a \to a'$ in $A$, where $a' = cod(\varphi(a, u))$, such that

• $\varphi$ defines a choice of lifts: $f \varphi(a, u) = u$,

• $\varphi$ preserves identity morphisms: $\varphi(a, 1_{f a}) = 1_{a}$,

• $\varphi$ preserves composition: $\varphi(a, v \circ u) = \varphi(a', v) \circ \varphi(a, u)$ where $a' = cod(\varphi(a, u))$.

Properties

Proposition

A delta lens $(f, \varphi) : A \to B$ is equivalent to a functor $f \colon A \to B$ and a cofunctor $\varphi \colon A \nrightarrow B$ such that $f a = \varphi_{0} a$ for all objects $a \in A$, and $f \varphi_{1}(a \in A, u \colon fa \to b \in B) = u$.

Proof

See (Ahman-Uustalu 2017, Section 6) and (Clarke 2020).

Examples

• A delta lens between codiscrete categories is precisely a classical lens (in computer science); see (Johnson-Rosebrugh 2016, Proposition 4).

• Every function $A \to B$ yields a delta lens $disc(A) \rightarrow disc(B)$ between discrete categories.

• Every discrete opfibration is a delta lens whose lifting operation is determined by the unique opcartesian lifts. Conversely, a delta lens is a discrete opfibration if the equation $\varphi(a, f w) = w$ holds for all morphisms $w \colon a \to a'$ in $A$.

• A split Grothendieck opfibration is a delta lens whose chosen lifts are opcartesian morphisms.

• Dually, a split Grothendieck fibration $A \to B$ is a delta lens $A^{op} \to B^{op}$.

• Every split epimorphism of monoids with a chosen section is a delta lens, when the monoids a considered as categories with a single object.

• More generally, every bijective on objects functor with a chosen section is a delta lens.

Related concepts

• lens (in computer science)

References

The notion of delta lens was first defined in computer science as a generalization of the classical lenses between sets:

• Zinovy Diskin, Yingfei Xiong, Krzysztof Czarnecki, From State- to Delta-Based Bidirectional Model Transformations: the Asymmetric Case, Journal of Object Technology, 10, 2011 (doi:10.5381/jot.2011.10.1.a6)

The connection between delta lenses and split Grothendieck opfibrations was first explored in the paper:

• Michael Johnson, Robert Rosebrugh, Delta Lenses and Opfibrations, Electronic Communications of the EASST, 57, 2013 (doi:10.14279/tuj.eceasst.57.875)

The following paper details the connection between delta lenses and the classical lenses:

• Michael Johnson, Robert Rosebrugh, Unifying Set-Based, Delta-Based and Edit-Based Lenses, CEUR Workshop Proceedings, 1571, 2016 (pdf)

The characterisation of delta lenses in terms of functors and cofunctors first appeared in the paper:

• Danel Ahman, Tarmo Uustalu, Taking updates seriously, Proceedings of the Sixth International Workshop on Bidirectional Transformations (Bx 2017), CEUR Workshop Proceedings 1827 (2017) [pdf]

The notion of delta lens between internal categories as well as the link between cofunctors, delta lenses, and split Grothendieck opfibrations is developed in the papers:

• Bryce Clarke, Internal lenses as functors and cofunctors, EPTCS, 323, 2020 (doi:10.4204/EPTCS.323.13)

• Bryce Clarke, Internal split opfibrations and cofunctors, Theory and Applications of Categories, 35, 2020 (link)