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 \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

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:

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: