(This is an update on my Ethereum Protocol Fellowship. More updates can be found here ).


Given sets $A$ and $B$, a function $f: A \to B$ can be ‘lifted’ to a lens $\mathcal{G}: {A \choose 1}\to {B\choose 1}$ by specifying $\mathcal{G}$ as the pair of functions $(\lambda_v, \lambda_u)$ where

\[\begin{align} \lambda_v&: A \to B \\ \lambda_v&: a \mapsto f(a)\\[4ex] \lambda_u&: A \times 1 \to 1\\ \lambda_u&: (a, \star) \mapsto \star \end{align}\]

This makes it possible to write down payoff or utility functions as a lens. In fact, they can be seen as an open game with a trivial set of strategies $\Sigma_\mathcal{G} = \{\star\}$. Recall:


An open game $\mathcal{G}: {X \choose S}\to {Y\choose R}$ is composed of the following data:

  • A set of strategies $\Sigma_\mathcal{G}$
  • A play function $P_\mathcal{G}: \Sigma_\mathcal{G}\to CL((X, S), (Y, R)) $
  • A best response function $B: X \times (Y \to R) \to \text{Rel}( \Sigma_\mathcal{G})$


From which it is immediately obvious that when $\Sigma_\mathcal{G} = \{\star\}$ an open game is just a choice of a lens from $CL((X, S), (Y, R))$, where $CL(A, B)$ is the collection of lenses from $A$ to $B$. (I’m only considering lenses in the category of sets in this post)


As I started drawing more complicated diagrams for various auction types, I started using the fact that the category of open games has counits (see for example here), that is for each set $X$ there is a morphism $\varepsilon_X : (X, X) \to (1, 1)$ which can be drawn like this:



Since this is an open game itself, this means that information can be ‘sent back in time’. This helps with sending the result of a lifted utility function back to the players so that they can take it into consideration. While discussing this with Philipp, a question we ran into was: Is a lens with the output ‘sent back in time’ equivalent to a lens with the same data sent as feedback? Obviously, this cannot be true for completely polymorphic lenses since the types have to match. It thus becomes the question:


When is a lens $~\mathcal{G}: {X \choose S}\to {Y\choose R}$ composed with the counit on $Y$ equivalent to a lens $\mathcal{H}: {X \choose S\times Y}\to {1 \choose R}~~$?


In diagrams:


Or equivalently, when does the following equation hold:

\[(id_R \otimes \varepsilon_Y) \circ (\sigma_{YR} \otimes id_Y) \circ (\mathcal{G} \otimes id_Y) = \mathcal{G'}\]

(I’m not 100% confident this is a well-defined equation. Since I’m using $\mathcal{G}$ as a morphism, i’m emphatically in the category of lenses (or games), where objects are pairs of objects from Set. However, I am also composing with morphisms that work on single objects from Set, namely the symmetric braiding and identities. However, I will just assume that these are trivially morphisms in the category of lenses over Set by inserting the appropriate unitors and identities everywhere.)


Since a lens is given by a pair of functions, a minimum restriction for the above equivalence to hold in general is that the cardinalities of the set of possible functions match. Let $\mathcal{G} = (f_v, f_u)$ and $\mathcal{G’} = (f_v’, f_u’)$. Then we have:

\[\begin{align} |f_v: X \to Y|& = |Y|^{|X|}\\ |f_u: X \times R \to S| &= |S|^{|X\times R|}\\[4ex] |f_v': X \to 1| &= 1\\ |f_u': X \times R \to S \times Y| &= |S \times Y|^{|X\times R|} \end{align}\]

Matching the cardinalities of $(f_v, f_u)$ and $(f_v’, f_u’)$ is only possible if $R = \{\star\}$, so this puts a constraint on the types of lenses for which sending output back in time is the same as feedback. However, whenever $R = \{\star\}$, an equivalence between $\mathcal{G}$ and $\mathcal{G’}$ is easily constructed by defining functions of the following types:

\[\begin{align} f_v&: X \to Y\\ f_u&: X \times 1 \to S\\[4ex] f_v'&: X \to 1\\ f_u'&: X \times 1 \to S \times Y\\ \end{align}\]

Since $f’_v$ is the trivial function, all structure of $\mathcal{G}$ has to be encoded in $f’_u$. Do this as follows:

\[f_u': (x, \star) \xrightarrow{\Delta_X} ((x, x), \star) \xrightarrow{\alpha_{X, X, \star}} (x, (x, \star)) \xrightarrow{f_v \otimes f_u} (y, s) \xrightarrow{\sigma_{YS}} (s, y)\]

That is, $f_u’ = \sigma_{YS} \circ (f_v \otimes f_u) \circ \alpha_{X, X, \star}\circ \Delta_X $, where $\Delta_X$ is the copy map of $X$, $\alpha$ the associator of the monoidal product on Set, and $\sigma$ the symmetric braiding.

With this definition, $\mathcal{G}$ and $\mathcal{G}’$ describe the exact same maps, which makes the two lenses equivalent:



A special case is when $S=\{\star\}$, in which case this says that a lifted function sending its output back in time is the same as a copoint. In general this says that a game can send its output back as feedback whenever the game itself receives no information from the future. Intuitively, I guess this is because information from the future—by definition—arrives after the output is emitted, so while it can influence the feedback, it cannot influence the output. That means the symmetry between feedback and output is broken, and output can no longer be transformed into feedback.