delta lens




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 delta lens (f,φ):AB(f, \varphi) : A \to B from a category AA to a category BB consists of a functor f:ABf : A \to B together with a lifting operation sending each pair (aA,u:fabB)(a \in A, u : f a \to b \in B) to a morphism φ(a,u):aa\varphi(a, u) : a \to a' in AA, where a=cod(φ(a,u))a' = cod(\varphi(a, u)), such that

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

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

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



A delta lens (f,φ):AB(f, \varphi) : A \to B is equivalent to a functor f:ABf : A \to B and a cofunctor φ:AB\varphi : A \nrightarrow B such that fa=φ 0af a = \varphi_{0} a for all objects aAa \in A, and fφ 1(aA,u:fabB)=uf \varphi_{1}(a \in A, u : fa \to b \in B) = u.



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:

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

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

  • Danel Ahman, Tarmo Uustalu, Taking updates seriously, 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:

Last revised on July 4, 2021 at 19:33:25. See the history of this page for a list of all contributions to it.