The optic interpretation of c-lenses

Let $\mathbf{Cat}$ denote the category of categories. A c-lens is the categorical lens notion defined by functors $\textsc{Get}:S\to A$ and $\textsc{Put}:(\textsc{Get}\downarrow\mathrm{id}_A)\to S$ satisfying the c-lens laws. An optic is called lawful when it satisfies the corresponding optic laws, and it may be mixed when its source and target categories differ.

C-lens optic conjecture. C-lenses are the lawful, possibly mixed optics for some action on $\mathbf{Cat}$.

The preceding theorem identifies c-lens data with a functor into a Grothendieck construction and characterizes lawful c-lenses as coalgebras for a comonad. The conjecture proposes an action on $\mathbf{Cat}$ that realizes this description as concrete optics, although the paper notes that no natural location for the additional category $A'$ is currently apparent.