Contents

# Contents

## 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:

## 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 : A \to B$ and a cofunctor $\varphi : A \nrightarrow B$ such that $f a = \varphi_{0} a$ for all objects $a \in A$, and $f \varphi_{1}(a \in A, u : fa \to b \in B) = u$.

###### Proof

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

## 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:

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.