Dependent Optics

DOI10.4204/EPTCS.380.8arXiv2204.09547MaRDI QIDQ6150150FDOQ6150150

Authors: Pietro Vertechi 

Publication date: 5 March 2024

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

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.

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

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Title not available (Why is that?)
• Introduction to bicategories
• Introduction to extensive and distributive categories
• Lenses, fibrations and universal translations
• A 2-categories companion
• Monoidal Grothendieck construction
• Adhesive and quasiadhesive categories
• Compositional Game Theory

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)