In Lawful lenses we discussed how we could state a definition for generic lawful optics and we proved that lawful lenses are exactly constant complement lenses.

In this post we will revisit the ideas presented there in a more categorical fashion, but focusing on lenses in particular.

What we will present in this post is a series of results which were obtained at the third Statebox Summit with the collaboration of the partecipants, out of which I ought to mention Jules Hedges, David Spivak, Brendan Fong, Christina Vasilakopoulou, Eliana Lorch and Andre Knispel for taking active part in this discussion.

The category of lenses

Let’s start by defining the category of lenses. The objects of our category will be pairs of sets \((S, T)\), morphisms between \((S, T)\) and \((A, B)\) will be lenses of type \(Lens \, S \, T \, A \, B\), which are described by pairs of functions

\[g : S \to A \\ p : S \to B \to T\]

The composition of two morphisms, i.e. two lenses, \((g, p) : (S, T) \to (A, B)\) and \((h, q) : (A, B) \to (C, D)\) is a new lens \(Lens \, S \, T \, C \, D\) defined by functions

\[g_c : S \to C \\ g_c = g\, ; h \\\] \[p_c : S \to D \to T \\ p_c \, s \, d = p \, s \, (q \, (g \, s) \, d)\]

where \(p_c\) can be represented by the following diagram

SDgqApBT

where \(\bullet : S \to S \times S\) is the \(copy\) operation.

Given any object of our category, which is a pair \((S, T)\), the identity morphism on it is the lens \((g_{id}, p_{id}) : (S, T) \to (S, T)\) defined by

\[g_{id} : S \to S \\ g_{id} \, s = s\] \[p_{id} : S \to T \to T \\ p_{id} \, s \, t = t\]

It can be checked that the above definitions satisfy the axioms for a category.

Associated lenses

Given a generic lens \(L := (g, p) : (S, T) \to (A, B)\), we saw in Lawful lenses that we can define a set

\[M = \{ m \in B \to T \, | \, \exists \, s : S . \; m = p \, s \}\]

which turns out to be really helpful in proving that lawful lenses are exactly the constant complement ones. In fact, this set allows us to define two new lenses associated to the lens \(L\).

First off, we can define \(\tilde{L} : (S, T) \to (A \times M, B \times M)\) by

\[\tilde{g} : S \to A \times M \\ \tilde{g}\, s = (g \, s, p \, s)\] \[\tilde{p} : S \to B \times M \to T \\ \tilde{p} \, s \, (b, m) = m \, b\]

Moreover we can also define \(\hat{L} : (B \times M, A \times M) \to (T, S)\) by

\[\hat{g} : B \times M \to T \\ \hat{g} \, (b, m) = m \, b\] \[\hat{p} : B \times M \to S \to A \times M \\ \hat{p} \, (b, m) s = (g \, s, p \, s)\]

Notice how ^ (pronounced “hat”) produces a swap between \(A\) and \(B\) and between \(S\) and \(T\). In their generic form, \(\tilde{L}\) and \(\hat{L}\) are not composable. However, if we restrict them to simple lenses, they are!

So, with these two new lenses at hand, some questions arise naturally:

  • In the simple lens case, when are \(\tilde{L}\) and \(\hat{L}\) inverse of one another?
  • In the simple lens case, when are \(\tilde{L}\) and \(\hat{L}\) lawful?

  • In the generic case, if we consider \(\pi : (A \times M, B \times M) \to (A, B)\) to be the lens defined by

    \[g_{\pi} : A \times M \to A \\ g_{\pi} \, a \, m = a\] \[p_{\pi} : A \times M \to B \to B \times M \\ p_{\pi} \, (a, m) \, b = (b, m)\]

    is it always true that \(L = \tilde{L} \, ; \pi\)?

Are \(\tilde{L}\) and \(\hat{L}\) inverses?

Let us first consider the composition \(\tilde{L} \, ; \hat{L}\). In this case we have

\[g_{\hat{\sim}} : S \to S \\ g_{\hat{\sim}} \, s = p \, s \, g(s) = s \textrm{ --- by getput}\] \[p_{\hat{\sim}} : S \to S \to S \\ p_{\hat{\sim}} \, s_1 \, s_2 = p \, s_2 \, (g \, s_2) = s_2 \textrm{ --- by getput}\]

Therefore \(\tilde{L} \, ; \hat{L} = id_{(S, S)}\) if and only if \(getput\) holds for \(L\).

On the other hand, consider \(\hat{L} \, ; \tilde{L}\). We obtain

\[g_{\tilde{\wedge}} : A \times M \to A \times M \\ g_{\tilde{\wedge}} \, (a, m) = (g \, (m \, a), p \, (m \, a))\] \[p_{\tilde{\wedge}} : A \times M \to A \times M \to A \times M \\ p_{\tilde{\wedge}} \, (a_1, m_1) \, (a_2, m_2) = (g \, (m_2 \, a_2), p \, (m_2 \, a_2))\]

Remember that by definition of \(M\) we have that any \(m \in M\) is of the form \(p \, s\) for some \(s \in S\). Hence we get

\[g_{\tilde{\wedge}} : A \times M \to A \times M \\ \begin{aligned} g_{\tilde{\wedge}} (a, p \, s) &= (g \, (p \, s \, a), p \, (p \, s \, a)) \\ &= (a, p \, s) \textrm{ --- by putget and putput, respectively} \end{aligned}\] \[p_{\tilde{\wedge}} : A \times M \to A \times M \to A \times M \\ \begin{aligned} p_{\tilde{\wedge}} (a_1, p \, s_1) (a_2, p \, s_2) &= (g \, (p \, s_2 \, a_2), p \, (p \, s_2 \, a_2)) \\ &= (a_2, p \, s_2) \textrm{ --- by putget and putput, respectively} \end{aligned}\]

We then obtain that \(\hat{L} \, ; \tilde{L} = id_{(M \times A, M \times A)}\) whenever \(L\) satisfies \(putget\) and \(putput\).

We conclude by saying that \(\tilde{L}\) and \(\hat{L}\) are each other’s inverses if and only if \(L\) is a lawful lens.

Are \(\tilde{L}\) and \(\hat{L}\) lawful?

In this section we will check whether \(\tilde{L}\) and \(\hat{L}\) are lawful lenses in the simple case, and which conditions we do need to assume on \(L\) for them to satisfy the lens laws.

Let’s start with \(\tilde{L}\)

getput:

\[\tilde{p} \, s \, (\tilde{g} \, s) = p \, s \, (g \, s) = s \textrm{ --- by getput}\]

putget:

\[\begin{aligned} \tilde{g} \, (\tilde{p} \, s_1 \, (a, p \, s_2)) &= \tilde{g} \, (p\, s_2 \, a) \\ &= (g \, (p \, s_2 \, a), p \, (p \, s_2 \, a)) \\ &= (a, p \, s_2) \textrm{ --- by putget and putput} \end{aligned}\]

putput:

\[\begin{aligned} \tilde{p}\, (\tilde{p} \, s \, (a_1, m_1)) \, (a_2, m_2) &= \tilde{p} \, (m_1 \, a_1) \, (a_2, m_2) \\ &= m_2 \, a_2 \\ &= \tilde{p} \, s \, (a_2, m_2) \textrm{ --- always holds} \end{aligned}\]

Hence \(\tilde{L}\) always satisfies \(putput\), satisfies \(getput\) if \(L\) satisfies \(getput\) and satisfies \(putget\) if \(L\) satisfies \(putget\) and \(putput\). Therefore \(\tilde{L}\) is lawful if and only if \(L\) is.

Let’s now have a look at \(\hat{L}\)

getput:

\[\begin{aligned} \hat{p} \, (a, p \, s) \, (\hat{g}(a, p \, s)) &= \hat{p} \, (a, p \, s)(p \, s \, a) \\ &= (g \, (p \, s \, a), p \, (p \, s \, a)) \\ &= (a, p \, s) \textrm { --- by putget and putput, respectively} \end{aligned}\]

putget:

\[\begin{aligned} \hat{g} \, (\hat{p} \, (a, m) \, s) &= \hat{g} \, (g \, s, p \, s) \\ &= p \, s (g \, s) \\ &= s \textrm{ --- by getput} \end{aligned}\]

putput:

\[\begin{aligned} \hat{p} \, (\hat{p} \, (a, m) \, s_1) \, s_2 &= \hat{p} \, (g \, s_1, p \, s_1) \, s_2 \\ &= (g \, s_2, p \, s_2) \\ &= \hat{p} \, (a, m) \, s_2 \textrm{ --- always} \end{aligned}\]

Therefore also \(\hat{L}\) always satisfies \(putput\), and it satisfies \(getput\) if \(L\) satisfies \(putget\) and \(putput\) and satisfies \(putget\) if \(L\) satisfies \(getput\). So also \(\hat{L}\) is lawful if and only if \(L\) is.

Decomposing \(L\)

One question remains: whether \(L = \tilde{L} \, ; \pi\) holds. It is not hard to check that it actually always does; in fact if we compute \(g^{\circ}\) and \(p^{\circ}\) for the composed lens, we get

\[g^{\circ} : S \to A \\ g^{\circ} s = g_{\pi} \, (\tilde{g} \, s) = g_{\pi} \, (g \, s, p \, s) = g \, s\] \[p^{\circ} : S \to B \to T \\ \begin{aligned} p^{\circ} \, s \, b &= \tilde{p} \, (s, p_{\pi} \, (\tilde{g} \, s, b)) \\ &= \tilde{p} \, (s, p_{\pi} \, ((g \, s, p \, s), b)) \\ &= \tilde{p} \, (s, (b, p \, s)) = p \, s \, b \end{aligned}\]

In conclusion, we can always decompose \(L\) into \(\tilde{L} \, ; \pi\), where \(\pi\) is always lawful.

Conclusion

In this post we investigated the role of \(M\) more closely, as well as the lenses \(\tilde{L}\) and \(\hat{L}\) which are generated from it. We saw that \(\tilde{L}\) and \(\hat{L}\) are strictly related to \(L\), and that they satisfy the lens laws only if \(L\) satisfies other lens laws.

Putting together the three results presented above, we can also recover a more formal proof that a simple lens is lawful if and only if it is isomorphic to a constant complement lens.

Some further questions we might consider:

  • what is \(M\) for \(\tilde{L}\) and \(\hat{L}\)?
  • how are \(\tilde{\tilde{L}}\), \(\hat{\tilde{L}}\), \(\tilde{\hat{L}}\) and \(\hat{\hat{L}}\) related to \(L\), \(\tilde{L}\) and \(\hat{L}\)?
  • is there a relation between \(M\) being a singleton set and isomorphisms in the category of lenses (it is easy to prove that \(M = \{*\}\) implies that \(L\) satisfies \(putput\))?
  • are the properties stated for the simple case generalizable to the general case?