Higher Lenses

Posted on 29 April 2014 by Paolo Capriotti

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 $A$ and $B$ , a lens from $A$ to $B$ is given by the following data:

a function $g : A \to B$ , the “getter”;
a function $s : A \to B \to A$ , the “setter”;

subject to the following laws:

$gs : (a : A)(b : B) \to g (s(a,b)) = b$
$sg : (a : A) \to s(a, g(a)) = a$
$ss : (a : A)(b, b' : B) \to s(s(a, b), b') = s(a, b')$

$gs$ says that we get what we put in, $sg$ says that updating with the current value doesn’t do anything, $ss$ says that if we update twice, only the last update counts.

This definition makes sense for general types $A$ and $B$ , 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 $(g, s)$ as a coalgebra of the costate $(\infty, 1)$ -comonad $W_B$ defined by:

$W_B X = B \times (B \to X)$

The laws that we specified are only enough to show that $(g, s)$ is a $1$ -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 $(\infty, 1)$ -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 $g : A \to B$ is the getter of a lens if we can “coherently move” between any two fibres of $g$ . This can be made precise by asking that $g$ is the pullback of some map $g' : A' \to \| B \|$ along the projection $[-] : B \to \| B \|$ .

So we arrive at the following definition: a higher lens is a function $g : A \to B$ such that the family of fibres of $g$ :

$\mathsf{fib}_g : B \to \mathcal{U}$

factors through $\| B \|$ .

At this point, we need to show that for any two sets $A$ and $B$ , a higher lens from $A$ to $B$ is the same as a lens.

Suppose $g : A \to B$ is a higher lens, and let $h : \| B \| \to \mathcal{U}$ be a morphism that factors $\mathsf{fib}_g$ . Given $b, b' : B$ , we have that

$[b] = [b'].$

By applying $h$ we get an equivalence $e_{b, b'}$ between $\mathsf{fib}_g(b)$ and $\mathsf{fib}_g(b')$ .

Therefore, for any $a : A$ and $b : B$ , we get:

$e_{g(a), b}(a , \mathsf{refl}) : (a' : A) \times (g a' = b).$

We can now define:

$(s(a, b), gs(a, b)) :\equiv e_{g(a), b}(a, \mathsf{refl})$

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

To get the other laws, we observe that the $e_{b, b'}$ are coherent, i.e. given $b_1, b_2, b_3 : B$ ,

$e_{b_2, b_3} \circ e_{b_1, b_2} = e_{b_1, b_3},$

from which the third law follows easily. For the second law, it is enough to observe that coherence implies that $e_{b, b}$ is the identity.

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

Now, let $A$ and $B$ be sets, and $(g, s, gs, sg, ss)$ a lens from $A$ to $B$ . The family of fibres of $g$ can be thought of as having values in the universe $\mathcal{U}_0$ of sets, which is a 1-type. We are now left with the problem of factoring the map $f = \mathsf{fib}_g$ from $B$ to a 1-type through $\| B \|$ .

Nicolai Kraus and I are currently working on a paper on precisely the topic of factoring maps through truncations, where we give, for any $n$ and $m$ , a necessary and sufficient condition for a map from some type $X$ to an $m$ -type to factor through $\|X\|_n$ .

In our case, we have $n = -1$ and $m = 1$ , and in this particular example, the condition is as follows: we first need a “0-constancy” proof for $f$ :

$c_0 : (b_1, b_2 : B) \to f(b_1) = f(b_2)$

and then a “coherence” property for $c_0$ :

$c_1 : (b_1, b_2, b_3 : B) \to c_0(b_1, b_2) \cdot c_0(b_2, b_3) = c_0(b_1, b_3).$

Together, $c_0$ and $c_1$ form what we call a “1-constancy” proof for $f$ .

To show that $\mathsf{fib}_g$ is 1-constant, we begin by defining a map between any two fibres of $g$ :

$h : (b_1, b_2 : B) \to \mathsf{fib}_g(b_1) \to \mathsf{fib}_g(b_2)$

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

$u : (b : B) \to h(b, b) = \mathsf{id}$

$v : (b_1, b_2, b_3 : B) \to h(b_2, b_3) \circ h(b_1, b_2) = h(b_1, b_3).$

These can be obtained simply by reversing the above derivation of a lens from a higher lens and using the fact that both $A$ and $B$ are sets. Now, $h(b_1, b_2)$ is easily seen to be an equivalence (its inverse being $h(b_2, b_1)$ ), giving $c_0$ , and then $c_1$ follows directly from $v$ .

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.

This entry was posted in Applications. Bookmark the permalink.

17 Responses to Higher Lenses

Twan van Laarhoven says:

29 April 2014 at 10:07

A lens from A to B can also be represented by the type

Lens A B = exists C. Iso A (B × C)

Where Iso represents isomorphisms. The lens laws are equivalent to the laws of isomorphisms.

In HoTT the Iso could be replaced with equivalence or even equality (by univalence). I haven’t given it much thought, and I don’t understand much of the category theoretic language used in this post, so I don’t know what happens to higher paths. Also one problem of this definition is that it is large.

Reply
- Paolo Capriotti says:
  
  29 April 2014 at 10:17
  
  Yes, this is the intuition behind my definition: I’m trying to capture the idea that $g : A -> B$ is a “trivial” fibration (in the sense that it’s a product, not that it’s acyclic).
  
  However, I don’t think you can really take that as the definition, since it doesn’t work when A and B are empty (you get the whole universe instead of the unit type).
  
  Reply
spitters37 says:

29 April 2014 at 10:14

How does this connect to dependent lenses ?

Reply
- Paolo Capriotti says:
  
  29 April 2014 at 10:42
  
  I didn’t know about that development. Interesting.
  
  In any case, the lenses I defined in this post are non-dependent. I’m actually not sure what dependent lenses should actually be, since any function $g: A \to B$ could be considered as the getter of one (you can always express $A$ as a sigma type of the fibres of $g$ ).
  
  Reply
Andrea Vezzosi says:

30 April 2014 at 15:40

As an example, what would g’ : A’ -> || B || be if we take g to be g : X x Y -> X; g = fst ?

Also, is this way of getting around the need for coherence laws an instance of a more general technique?

Reply
- Paolo Capriotti says:
  
  30 April 2014 at 16:14
  
  My reply is below.
  
  Reply
Paolo Capriotti says:

30 April 2014 at 16:12

For $g : X \times Y \to X$ , the fibres are all equivalent to $Y$ , so $g'$ is just $\| X \| \times Y \to \| X \|$ , corresponding to the map $\| X \| \to \mathcal{U}$ constant at $X$ .

I don’t think this is an instance of a general technique. Sometimes, there really is no way of avoiding coherences, which usually means that you cannot work internally anymore, at least not until we figure out a way to internalise semi-simplicial sets or similar constructions.

In this case, we are lucky, since we can reduce the particular tower of “coherence properties” we want to asking that a certain map be “constant” in a strong sense (i.e. factor through the -1-truncation of its domain). In practice, however, expressing such a constancy property explicitly would require you to go back to the infinite tower of coherences (at least in the case where you make no assumptions on the truncation levels of the types involved).

Reply
Mike Shulman says:

1 May 2014 at 01:22

I don’t suppose your necessary and sufficient conditions for factoring through truncations will apply to the case $m=\infty$ ?

Reply
- Paolo Capriotti says:
  
  1 May 2014 at 02:43
  
  They do, with some caveats.
  
  The idea (for $n = -1$ ) is as follows: given a type $X$ , we can construct a corresponding semi-simplicial type in two ways. One is to make it into a 0-coskeletal semi-simplicial type $t X$ (whose component at level $i$ is simply $X^{i+1}$ ). The other is to take the constant presheaf at $X$ and then take a Reedy fibrant replacement (for which we use an explicit construction). Let’s denote this by $e X$ .
  
  Then, a function $f : X \to Y$ factors through $\| X \|$ if and only if it can be extended to a presheaf morphism $t X \to e Y$ . This turns into a tower of coherence conditions for $f$ , which can be simplified to a finite one when $Y$ is $m$ -truncated.
  
  We still have to work out some of the details of the proof, so I’m currently not particularly confident about the exact requirements. We definitely need Reedy limits of towers, and the general case $n > -1$ uses certain HITs. We also use strict functoriality of path objects quite liberally, but that could possibly be avoided.
  
  Reply
  - Mike Shulman says:
    
    1 May 2014 at 10:45
    
    Right, that’s what I would expect. That construction for n=-1,0 and m=0,1 can essentially be found in the book (m=0 via exactness of the category of sets, so that $\Vert A\Vert$ can be constructed as the set-coequalizer of $A\times A \rightrightarrows A$ , and m=1 via the Rezk completion, with 1-types viewed as groupoids). Mainly I was wondering whether you’d found a way to express the infinitely many coherence conditions for $m=\infty$ internally; but if you can express the case of finite m as an internal function of m, that’s pretty impressive too!
    
    Reply
    - Paolo Capriotti says:
      
      2 May 2014 at 10:25
      
      How do you use the Rezk completion to prove the factorization property for $m = 1$ ? I’m afraid don’t see it. I’m also not sure about the argument for $m = 0$ , because $A$ doesn’t need to be a set for $f : A \to B$ to factor through $\| A \|$ , but maybe I just misunderstood what you meant.
      
      Unfortunately, we cannot express the case of finite $m$ as an internal function of $m$ . Actually, I think that if we had that, we could easily express the $m = \infty$ case as well, since Reedy limits of “internal” towers do always exist.
      
      We have been toying with the idea of writing some code generator that would give us the statement (and proof!) for any fixed $n$ and $m$ , so that you could plug it into a proof assistant and use it in practice, assuming the truncations levels are known statically. I don’t know how useful/interesting that would be.
      
      To have a proper internal formulation of this result, I think we really need something like the universe of semi-simplicial types. I have been experimenting with adding ad-hoc rules into the syntax that would allow us to take Reedy limits over arbitrary (countable) inverse categories (as I briefly mentioned in a comment to your own post), but I’m still not sure if and how that would work.
      
      Reply
    - Mike Shulman says:
      
      2 May 2014 at 11:10
      
      I’m also not sure about the argument for $m = 0$ , because $A$ doesn’t need to be a set for $f : A \to B$ to factor through $\| A \|$
      
      Just 0-truncate it first: since B is a set, f automatically factors through $\|A\|_0$ .
      
      How do you use the Rezk completion to prove the factorization property for $m = 1$ ?
      
      For $n=-1$ and $m=1$ , let A be the codiscrete precategory with A as its type of objects, i.e. $\hom_{\mathbf{A}}(x,y) = \mathbf{1}$ for all x,y. Then the Rezk completion of A is the (-1)-truncation of A. Let B be the “discrete” category with B as its type of objects, i.e. $\hom_{\mathbf{B}}(x,y) = (x=y)$ for all x,y. Since B is a category, a functor $\hat{\mathbf{A}} \to \mathbf{B}$ can be induced by a functor $\mathbf{A} \to \mathbf{B}$ , which is basically what you called a “1-constancy proof”.
      
      For $n=0$ and $m=0$ , let A be instead the “discrete” precategory on A, with $\hom_{\mathbf{A}}(x,y) = \|x=y\|_{-1}$ . Now the Rezk completion of A is the 0-truncation of A.
      
      Unfortunately, we cannot express the case of finite $m$ as an internal function of $m$ . Actually, I think that if we had that, we could easily express the $m = \infty$ case as well
      
      I don’t see that; can you elaborate?
      
      Reply
      - Paolo Capriotti says:
        
        2 May 2014 at 11:44
        
        let $A$ be the codiscrete precategory with $A$ as its type of objects
        
        Oh, of course! Thanks. That’s exactly the specialization of our proof, by the way. I didn’t recognize the Rezk completion in there.
        
        I don’t see that; can you elaborate?
        
        Well, I meant that one can use coinduction to take the limit of such a tower of coherences. I’m not sure what is known about the existence of coinductive types in models of HoTT, so this might not be a big improvement, but at least we have some syntax to talk about such things.
        
        In fact, suppose the property is expressed by a term
        P : (n : Nat) -> E n -> Type
        where E satisfies:
        E 0 = 1 E (suc n) = Sigma (x : E n) . P n x
        definitionally.
        
        Then you could give a definition like:
        codata S (n : Nat)(x : E n) : Type where cons : (y : P n x) -> S (suc n) (x, y) -> S n x
        
        and S 0 * would give you the limit of the tower.
        
        Reply
      - Mike Shulman says:
        
        2 May 2014 at 11:49
        
        I mean, how do you know that the limit of that tower would give you the condition that works for $m=\infty$ ?
        
        Reply
        
        Paolo Capriotti says:
        
        2 May 2014 at 11:56
        
        Oh, that’s what we prove (assuming all the details work out… as I said, it’s work in progress): the type $\| A \| \to B$ is equivalent (over $A \to B$ ) to the Reedy limit of a certain tower, provided such limit exists.
        
        The way I phrased it was indeed weaker, but this is the formulation we are aiming for.
        
        Reply
        
        Mike Shulman says:
        
        2 May 2014 at 14:10
        
        Okay; I look forward to seeing the proof! I can’t think of a way to prove that without having a “geometric realization” for untruncated simplicial objects, which at least naively would be a HIT with infinitely many constructors.
        
        Reply
        
        spitters37 says:
        
        2 May 2014 at 15:42
        
        There is a new paper on lenses at TYPES.
        
        Reply