论文标题
通过更高类别理论的镜头和光学的时空权衡
Space-time tradeoffs of lenses and optics via higher category theory
论文作者
论文摘要
光学和镜头是抽象的分类小工具，它们以双向数据流进行建模。在本文中，我们观察到，光学的表示定义 - 通过从外部观察它们的行为来识别两个光学元件 - 不适用于操作，面向软件的方法，不仅可以观察到光学器件，而且还以其内部设置为基础。我们确定了笛卡尔光学和镜头的表示同构类别之间的操作差异：它们的不同组成规则和相应的时空折衷方案，将它们定位在光谱的两个相对端。通过这些动机，我们将现有的分类结构及其关系提升到了两类水平，表明相关的操作问题变得可见。我们定义2类别$ \ textbf {2-optic}（\ Mathcal {c}）$，其2细胞明确跟踪Optics的内部配置。我们表明，1类别$ \ textbf {optic}（\ mathcal {c}）$通过本地列出此2类别的连接组件而产生。我们表明，将镜头嵌入到笛卡尔光学器件中，从函子到oplax函子，其oplaxator现在检测到不同的组成规则。我们确定显示该函子在任何标准2类中构成邻接的一部分的困难。我们确定了一个猜想，即笛卡尔镜头和光学之间的众所周知的同构是由于其双类别对应物之间的宽松2次结构而产生的。除了介绍新的研究外，本文还旨在对该主题进行访问。
Optics and lenses are abstract categorical gadgets that model systems with bidirectional data flow. In this paper we observe that the denotational definition of optics - identifying two optics as equivalent by observing their behaviour from the outside - is not suitable for operational, software oriented approaches where optics are not merely observed, but built with their internal setups in mind. We identify operational differences between denotationally isomorphic categories of cartesian optics and lenses: their different composition rule and corresponding space-time tradeoffs, positioning them at two opposite ends of a spectrum. With these motivations we lift the existing categorical constructions and their relationships to the 2-categorical level, showing that the relevant operational concerns become visible. We define the 2-category $\textbf{2-Optic}(\mathcal{C})$ whose 2-cells explicitly track optics' internal configuration. We show that the 1-category $\textbf{Optic}(\mathcal{C})$ arises by locally quotienting out the connected components of this 2-category. We show that the embedding of lenses into cartesian optics gets weakened from a functor to an oplax functor whose oplaxator now detects the different composition rule. We determine the difficulties in showing this functor forms a part of an adjunction in any of the standard 2-categories. We establish a conjecture that the well-known isomorphism between cartesian lenses and optics arises out of the lax 2-adjunction between their double-categorical counterparts. In addition to presenting new research, this paper is also meant to be an accessible introduction to the topic.
