Lenses are a very powerful and practically useful functional construct. They represent “first class” fields for a data structure.

Lenses arose in work on bidirectional programming (for example, in Boomerang), and in Haskell, people have given many different definitions of lenses, but the simplest and easiest to replicate in type theory is probably the one based on getters and setters.

Given types *lens* from

- a function
, the “getter”; - a function
, the “setter”;

subject to the following laws:

This definition makes sense for general types

The problem with this definition becomes apparent if, following Russell O’Connor, we think of the pair

The laws that we specified are only enough to show that

Unfortunately, it is not yet clear how to define

One possible idea is the following: a function

So we arrive at the following definition: a *higher lens* is a function

factors through

At this point, we need to show that for any two *sets*

Suppose

By applying

Therefore, for any

We can now define:

and obtain the setter and the first law at the same time.

To get the other laws, we observe that the *coherent*, i.e. given

from which the third law follows easily. For the second law, it is enough to observe that coherence implies that

So, any higher lens is also a lens, regardless of truncation levels.

Now, let

Nicolai Kraus and I are currently working on a paper on precisely the topic of factoring maps through truncations, where we give, for any

In our case, we have

and then a “coherence” property for

Together,

To show that

and showing that it is functorial, in the sense that we have functions:

These can be obtained simply by reversing the above derivation of a lens from a higher lens and using the fact that both

We haven’t shown that these two mappings are inverses of each other. I haven’t checked this in detail, but I think it’s true. To prove it, one would need to rearrange the above proof into a chain of simple equivalences, which would directly show that the two notions are equivalent.