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 and , a lens from to is given by the following data:
- a function , the “getter”;
- a function , the “setter”;
subject to the following laws:
says that we get what we put in, says that updating with the current value doesn’t do anything, says that if we update twice, only the last update counts.
This definition makes sense for general types and , and it’s straightforward to define composition for those lenses. However, as soon as we try to show – say – that composition is associative, we stumble upon “coherence” issues.
The problem with this definition becomes apparent if, following Russell O’Connor, we think of the pair as a coalgebra of the costate -comonad defined by:
The laws that we specified are only enough to show that is a -coalgebra, which is not a well-behaved notion, unless we restrict our attention to sets (i.e. 0-truncated types).
Unfortunately, it is not yet clear how to define -categorical concepts internally in HoTT, but we can try to restructure the definition to work around the need to deal with higher coherences.
One possible idea is the following: a function is the getter of a lens if we can “coherently move” between any two fibres of . This can be made precise by asking that is the pullback of some map along the projection .
So we arrive at the following definition: a higher lens is a function such that the family of fibres of :
factors through .
At this point, we need to show that for any two sets and , a higher lens from to is the same as a lens.
Suppose is a higher lens, and let be a morphism that factors . Given , we have that
By applying we get an equivalence between and .
Therefore, for any and , we get:
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 are coherent, i.e. given ,
from which the third law follows easily. For the second law, it is enough to observe that coherence implies that is the identity.
So, any higher lens is also a lens, regardless of truncation levels.
Now, let and be sets, and a lens from to . The family of fibres of can be thought of as having values in the universe of sets, which is a 1-type. We are now left with the problem of factoring the map from to a 1-type through .
Nicolai Kraus and I are currently working on a paper on precisely the topic of factoring maps through truncations, where we give, for any and , a necessary and sufficient condition for a map from some type to an -type to factor through .
In our case, we have and , and in this particular example, the condition is as follows: we first need a “0-constancy” proof for :
and then a “coherence” property for :
Together, and form what we call a “1-constancy” proof for .
To show that is 1-constant, we begin by defining a map between any two fibres of :
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 and are sets. Now, is easily seen to be an equivalence (its inverse being ), giving , and then follows directly from .
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.