Dependent Optics

DOI10.4204/EPTCS.380.8MaRDI QIDQ6150150FDO

Authors Pietro Vertechi

Publication date 5 March 2024

Published in Electronic Proceedings in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2204.09547

Mathematics Subject Classification ID

Computer science (68-XX)

Abstract: A wide variety of bidirectional data accessors, ranging from mixed optics to functor lenses, can be formalized within a unique framework--dependent optics. Starting from two indexed categories, which encode what maps are allowed in the forward and backward directions, we define a category of dependent optics and establish under what assumptions it has coproducts. Different choices of indexed categories correspond to different families of optics: we discuss dependent lenses and prisms, as well as closed dependent optics. We introduce the notion of Tambara representation and use it to classify contravariant functors from the category of optics, thus generalizing the profunctor encoding of optics to the dependent case.

Recommendations

• Profunctor optics, a categorical update
• Towards optic-based algebraic theories: the case of lenses
• Bidirectional processes -- in category theory, physics, engineering, \dots
• Internal lenses as functors and cofunctors
• Cornering Optics

Cites work

• scientific article; zbMATH DE number 1840601 (Why is no real title available?)
• A 2-categories companion
• Adhesive and quasiadhesive categories
• Compositional game theory
• Introduction to bicategories
• Introduction to extensive and distributive categories
• Lenses, fibrations and universal translations
• Monoidal Grothendieck construction

Cited in

(4)

• Coend Optics for Quantum Combs
• Cornering Optics
• Towards optic-based algebraic theories: the case of lenses
• Profunctor optics, a categorical update

This page was built for publication: Dependent Optics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6150150)