Abstract
Optics and lenses are abstract categorical gadgets that model systems withbidirectional data flow. In this paper we observe that the denotationaldefinition of optics - identifying two optics as equivalent by observing theirbehaviour from the outside - is not suitable for operational, software orientedapproaches where optics are not merely observed, but built with their internalsetups in mind. We identify operational differences between denotationallyisomorphic categories of cartesian optics and lenses: their differentcomposition rule and corresponding space-time tradeoffs, positioning them attwo opposite ends of a spectrum. With these motivations we lift the existingcategorical constructions and their relationships to the 2-categorical level,showing that the relevant operational concerns become visible. We define the2-category $\textbf{2-Optic}(\mathcal{C})$ whose 2-cells explicitly trackoptics' internal configuration. We show that the 1-category$\textbf{Optic}(\mathcal{C})$ arises by locally quotienting out the connectedcomponents of this 2-category. We show that the embedding of lenses intocartesian optics gets weakened from a functor to an oplax functor whoseoplaxator now detects the different composition rule. We determine thedifficulties in showing this functor forms a part of an adjunction in any ofthe standard 2-categories. We establish a conjecture that the well-knownisomorphism between cartesian lenses and optics arises out of the lax2-adjunction between their double-categorical counterparts. In addition topresenting new research, this paper is also meant to be an accessibleintroduction to the topic.