Categories of Optics

Abstract

Bidirectional data accessors such as lenses, prisms and traversals are all instances of the same general 'optic' construction. We give a careful account of this construction and show that it extends to a functor from the category of symmetric monoidal categories to itself. We also show that this construction enjoys a universal property: it freely adds counit morphisms to a symmetric monoidal category. Missing in the folklore is a general definition of 'lawfulness' that applies directly to any optic category. We provide such a definition and show that it is equivalent to the folklore profunctor optic laws.

arXiv comment51 pages. v2: typos/minor fixes

References in corpus (1)

• Doubles for monoidal categories

Cited by in corpus (13)

• DisCoPy: Monoidal Categories in Python
• Profunctor Optics, a Categorical Update
• Open Diagrams via Coend Calculus
• Bayesian Updates Compose Optically
• Comb Diagrams for Discrete-Time Feedback
• Category Theory in Machine Learning
• Profunctor optics and traversals
• Generalized Lens Categories via functors ${\mathcal{C}}^{\mathrm{op}}\to \mathsf{Cat}$
• Translating Extensive Form Games to Open Games with Agency
• Bayesian open games
• Automatic Backward Filtering Forward Guiding for Markov processes and graphical models
• Cyber Kittens, or Some First Steps Towards Categorical Cybernetics
• The Safari of Update Structures: Visiting the Lens and Quantum Enclosures