On a fibrational construction for optics, lenses, and Dialectica categories
Matteo Capucci, Bruno Gavranović, Abdullah Malik, Francisco Rios, Jonathan Weinberger
TL;DR
The paper addresses unifying lenses, optics, and Dialectica morphisms under a single fibrational framework by iteratively dualizing towers of fibrations into dialenses. It shows that height $1$ dialenses correspond to lenses, while height $2$ dialenses capture optics and Dialectica morphisms, with higher heights generalizing further bidirectional data-flow patterns. The authors connect this dialense construction to Hofstra's Dial monad by showing $\mathbf{Dial}(P) = \mathbf{Sum}(\mathbf{Prod}(P)) = \mathbf{Sum}(\mathbf{Sum}(P)^{\vee})^{\vee}$, revealing Dialectica categories as a special case. This unified perspective clarifies the relationships among these formalisms and provides a scalable framework for modeling complex bidirectional interactions in category-theoretic terms.
Abstract
Categories of lenses/optics and Dialectica categories are both comprised of bidirectional morphisms of basically the same form. In this work we show how they can be considered a special case of an overarching fibrational construction, generalizing Hofstra's construction of Dialectica fibrations and Spivak's construction of generalized lenses. This construction turns a tower of Grothendieck fibrations into another tower of fibrations by iteratively twisting each of the components, using the opposite fibration construction.