Categories of lenses/optics and Dialectica categories are both comprised of bidirectional morphisms of basically the same form.
In this work we show how they can be considered a special case of an overarching fibrational construction, generalizing Hofstra's construction of Dialectica fibrations and Spivak's construction of generalized lenses.
This construction turns a tower of Grothendieck fibrations into another tower of fibrations by iteratively twisting each of the components, using the opposite fibration construction.

§ INTRODUCTION

As shown in prior work, on various levels of generality, one can generalize de Paiva's dependent Dialectica category construction <cit.>, which assigns to a finitely complete category $\cat C$ the (dependent) Dialectica category $\mathfrak{Dial}(\cat C)$ as follows. The latter can be shown to be equivalent to an iterated completion by sums and products, resp., so that we have an equivalence $\mathfrak{Dial}(\cat C) \simeq \Sigma \Pi(\cat C)$. When generalizing to a fibration $P: \cat E \to \cat B$ of categories, which captures the idea of a family of categories, varying over a base category, one therefore uses the analogous completion constructions but on the level of fibrations. We will always work over a base $\cat B$ with finite limits. The fibered or dependent sum completion (also $\Sigma$-completion) of a fibration $P: \cat E \to \cat B$ is given by pulling back the fibration $P$ along the domain fibration $\dom: \cat B^\downarrow \to \cat B$ and then postcomposing with the codomain fibration $\cod: \cat B^\downarrow \to \cat B$:

\[\begin{tikzcd}
{\Sigma \cat E} && {\cat E} \\
{\cat B^\to} && {\cat B} \\
{\cat B}
\arrow["{\dom}"', from=2-1, to=2-3]
\arrow[from=1-1, to=2-1]
\arrow[from=1-1, to=1-3]
\arrow["{P}", from=1-3, to=2-3]
\arrow["{\cod}", from=2-1, to=3-1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-3]
\arrow["{\Sigma P}"', curve={height=30pt}, from=1-1, to=3-1]
\end{tikzcd}\]

The dual process, completing by dependent products, is given by considering the dual fibration $\dual{P}$ of $P$ that dualizes the fibers of $P$, then applying the $\Sigma$-completion, and then taking the dual of this result again, so $\Pi(P) = \dual{\Sigma(\dual{P})}$. The dependent Dialectica fibration over the given fibration $P$ is then
$\mathfrak{Dial}(P) = \Sigma \Pi (P)$. So far, this has been known due to (the cumulated) work by Hyland <cit.>, Biering <cit.>, Hofstra <cit.>, von Glehn <cit.>, Moss <cit.>, and Moss–von Glehn <cit.> (see also <cit.> for an internal characterization). In the work at hand, we are providing a common generalization of the Dialectica construction and optics <cit.> that in applied category theory and categorical systems theory <cit.> model processes of computation of bidirectional information processing, involving a “black-boxed” part where information is processed internally. In its categorical specification this is modeled through a monoidal structure. A special case of both Dialectica and optics is the case of lenses which are exactly the special case of Dialectica where one trivializes the logical predicate or, the special case of optics where one loses the internal computation.
We have achieved this by using iterated duals, taking over sequences of $n$ composable fibrations (with the height $n$ varying).

Let $\mathbf{P} = (\cat E_n \stackrel{P_n}{\to} \mathsf \cat E_{n-1} \stackrel{P_{n-1}}{\to} \ldots \stackrel{P_1}{\to} \cat E_0)$ be a sequence of $n$ composable fibrations. The $n$-fold dual over the sequence $\mathbf P$ is defined inductively as follows: for $n=1$, the usual dual, writing,

\[ \dual[1]{(\cat E_1 \stackrel{P_1} {\longrightarrow} \cat E_0)} := \dual[{\cat E_0}]{(\cat E_1)} \stackrel{\dual[\cat E_0]{P_1}}{\longrightarrow} \cat E_0 := (\cat E_1)^{\vee} \stackrel{\dual{P_1}}{\longrightarrow} \cat E_0 \]

and for $n=k+1$:

\[ \dual[k+1]{(\cat E_{k+1} \stackrel{P_{k+1}}{\longrightarrow} \ldots \stackrel{P_{2}}{\longrightarrow} \cat E_{1} \stackrel{P_{1}}{\longrightarrow} \cat E_{0})} = \dual[k]{\dual[\cat E_0]{(\cat E_{k+1} \substack{p_{k+1}}{\longrightarrow} \ldots \cat E_1)}} \stackrel{\dual[\cat E_0]{p_1}}{\longrightarrow} \cat E_0. \]

A morphism in $\dual[n]{\cat E_n}$ is called a $\mathbf{P}$-dialens of height $n$.

We show that the notion of $\mathbf{P}$-dialens of height $n$ provides a joint generalization of (dependent) lenses, Dialectica, and optics in the following sense.
[Dialenses as generalized categorical data structures]

* $P$-lenses are dialenses of height $1$.

* $P$-Dialectica categories (either simple or dependent) are dialenses of height $2$.

* Optics are dialenses of height $2$, coming from the Para construction over the given base symmetric monoidal category.

§.§ Acknowledgments

We would like to thank Valeria de Paiva for her outstanding and sustained mentorship at the 2022 American Mathematical Society Mathematics Research Community (AMS MRC) and beyond, as well as for providing feedback and corrections to a draft version of this text. Furthermore, we are grateful to numerous fruitful discussions with our other team members Charlotte Aten, Colin Bloomfield, Eric Bond, Joseph Dorta, Samantha Jarvis, Jérémie Koenig, Nelson Niu, and Jan Rooduijn. This material is based upon work supported by the National Science Foundation under Grant Numbers
DMS 1641020 and DMS 1916439. Any opinions, findings, and conclusions or recommendations expressed in this material
are those of the authors and do not necessarily reflect the views of the National Science Foundation.

JW is grateful for financial support by the US Army Research Office under MURI
Grant W911NF-20-1-0082, and for hospitality and financial support provided by the Max Planck Institute for Mathematics, Bonn, Germany.

§ PRELIMINARY NOTIONS ON FIBRATIONS

Let $P: \cat E \to \cat B$ be a functor. For an object $X \in \cat B$, we define the fiber of $P$ at $X$ as the subcategory $P^{-1}(X)$ of $\cat E$ consisting of those morphisms $\varphi$ in $\cat E$ such that $p(\varphi) = \id_X$. A morphism in a fiber $p^{-1}(X)$ is called vertical.

Let $P: \cat E \to \cat B$. A morphism $\varphi : W \to V$ in $\cat E$ is $P$-cartesian if it satisfies the following universal property: let us write $\varphi := P(f)$ and $\varphi : X \to Y$ in $\cat B$. Then we demand that for any $g : Z \to X$ in $\cat B$ and any $g' : U \to V$ in $\cat E$ with $p(g') = f \comp g$, there exist a unique morphism $h : U \to W$ in $\cat E$ with $p(h) = g$ and $h \comp \varphi = g'$:

\begin{equation}
\begin{tikzcd}[ampersand replacement=\&, sep=4ex]
U \\
Z \& W \& \& V \\
\& X \& \& Y
\arrow[dotted, maps to, from=2-2, to=3-2]
\arrow["{{\exists ! h}}"', from=1-1, to=2-2]
\arrow[dotted, maps to, from=1-1, to=2-1]
\arrow["{{\forall g}}"', curve={height=6pt}, from=2-1, to=3-2]
\arrow["f", from=3-2, to=3-4]
\arrow["\varphi", from=2-2, to=2-4]
\arrow[dotted, maps to, from=2-4, to=3-4]
\arrow["{{\forall g'}}"{description}, curve={height=-24pt}, from=1-1, to=2-4]
\end{tikzcd}
\end{equation}

A Grothendieck fibration (or fibration for short) is a functor $P:\cat E \to \cat B$ such that any arrow $f:X \to P(V)$ in $\cat B$ admits a (strong) cartesian lift:

\begin{equation}
% https://q.uiver.app/#q=WzAsNixbMSwxLCJYIl0sWzIsMSwiUChWKSJdLFsyLDAsIlYiXSxbMSwwLCJmXipWIl0sWzAsMSwiXFxjYXQgQiJdLFswLDAsIlxcY2F0IEUiXSxbMywyLCJmX1YiXSxbMCwxLCJmIl0sWzUsNCwiUCIsMl1d
\begin{tikzcd}[ampersand replacement=\&]
{\cat E} \& {f^*V} \& V \\
{\cat B} \& X \& {P(V)}
\arrow["{f_V}", from=1-2, to=1-3]
\arrow["f", from=2-2, to=2-3]
\arrow["P"', from=1-1, to=2-1]
\end{tikzcd}
\end{equation}

For $f_V$ to be a cartesian lift, it has to be terminal among all morphisms into $V$ and projecting down to $f$, see <Ref>. Moreover, we can show these lifts compose: the cartesian lifts of $f$ and $g$ compose to give the cartesian lift for $f \comp g$. Furthermore, up to vertical isomorphism, the cartesian lift $f_V : f^*V \to V$ is determined uniquely.

$\cat E$ is called the total category and $\cat B$ the base category.

We are going to assume that every fibration is cloven, i.e. comes equipped with a specific choice of cartesian lifts. A way to say this is that we have an indexed category $\de P$ and an isomorphism $\int \de P \iso P$.
In this way we can move freely between a fibration and its indexing of fibers.

Let $P : \cat E \to \cat B$ be a fibration.

* If $Q: \cat F \to \cat E$ is a fibration, then the composite functor $P \comp Q : \cat F \to \cat B$ is a fibration.

* If $Q: \cat F \to \cat B$ is any functor, then the pullback

\[\begin{tikzcd}[sep=4ex]
{Q^*\cat E} & {\cat E} \\
{\cat F} & {\cat B}
\arrow["{Q^*P}"', from=1-1, to=2-1]
\arrow["Q", from=2-1, to=2-2]
\arrow["P", from=1-2, to=2-2]
\arrow[from=1-1, to=1-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\end{tikzcd}\]

is a fibration.

Dualizing the notion of cartesian arrow gives rise to opcartesian arrows, and dualizing the notion of fibration yields Grothendieck opfibrations. In an opfibration $P: \cat E \to \cat B$, we can lift arrows $f : X \to Y$ given elements $U \in p^{-1}(X)$ to opcartesian arrows $U \to f_*U$ over $f$. While cartesian arrows satisfy a terminality property, opcartesian arrows satisfy an initiality property.

Like fibrations, opfibrations are closed under composition and pullback.

[Examples of fibrations]
For a category $\cat C$, we denote by $\cat C^\downarrow$ the category of morphisms in $\cat C$ with arrows given by the commutative squares.

* Domain fibration: For any category $\cat C$, the domain projection $\dom := \dom_{\cat C} : {\cat C}^\downarrow \to \cat C$ is a fibration. For $u:I \to J$ in $\cat B$, a cartesian lift of $u$ w.r.t. an arrow $g : J\to Y$ is given by the square:

\[\begin{tikzcd}[sep=4ex]
I & J \\
X & Y
\arrow["u\comp g"', from=1-1, to=2-1]
\arrow[Rightarrow, no head, from=2-1, to=2-2]
\arrow["u", from=1-1, to=1-2]
\arrow["g", from=1-2, to=2-2]
\end{tikzcd}\]

* Codomain fibration: If $\cat C$ has all pullbacks, then the codomain projection $\cod := \cod_{\cat C} : \cat C^\downarrow \to \cat C$ is a fibration, also called the fundamental fibration of $\cat C$. If $\cat C$ is locally cartesian closed, the codomain fibration gives rise to a model of dependent type theory with $\Sigma$- and $\Pi$-types <cit.>. The idea is to interpret a type $X$ in context (i.e., a list of free variables) $I$ as a morphism $X \to I$, hence an object of the slice $\cat C/I$, which is the fiber of $\cod$ at $I\in \cat C$.

Given an arrow $u : J \to I$ in $\cat C$ together with a map $p : X \to I$, a $\cod$-cartesian lift of $u$ w.r.t. $p$ is given by pullback:

\[\begin{tikzcd}[sep=4ex]
{u^*X} & X \\
J & I
\arrow["u", from=2-1, to=2-2]
\arrow["p", from=1-2, to=2-2]
\arrow[from=1-1, to=2-1]
\arrow[from=1-1, to=1-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\end{tikzcd}\]

This corresponds to substituting the variables in context $I$ along $u$.

* Simple fibration: Whereas the codomain fibration models arbitrary dependent types in context $I$, we might want to restrict to the case of simple types. A constant type is a dependent type over the terminal context $1$, hence a map $X \to 1$, or equivalently, just an object $X$. We can then view $X$ as a type over any context, by considering the pullback:

\[\begin{tikzcd}[sep=4ex]
{I \times X} & X \\
I & 1
\arrow[from=2-1, to=2-2]
\arrow[from=1-2, to=2-2]
\arrow[from=1-1, to=2-1]
\arrow[from=1-1, to=1-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\end{tikzcd}\]

Therefore, the simple fibration is the full subfibration of the codomain fibration $\cod_{\cat C}$, by restricting to product projections $I \times X \to I$. Up to fibered equivalence, the simple fibration can be constructed as follows. Let $\cat C$ be a category with all products. Then we define the category $\cat C^{\proj}$ by taking as objects pairs $(I,X)$ of $\cat C$ and as morphisms $(I,X) \to (J,Y)$ pairs of morphisms $(u : I \to J,f : I \times X \to J)$ in $\cat C$. The simple fibration $\times : \cat C^\downarrow_{\proj} \to \cat C$ is then the functor defined by $\times(I,X) := I$ and $\times(u,f) := u$. This is indeed a fibration, where a cartesian lift of $u : I \to J$ w.r.t $(J,Y)$ is given by the map $(u,\pi_Y): (I,Y) \to (J,Y)$ with $\pi_Y : I \times Y \to Y$.

* Subobject fibration: Let $\cat C$ have all pullbacks. We can consider the full subfibration

\[\begin{tikzcd}[sep=4ex]
{\cat C_{\mathrm{mono}}^\downarrow} && {\cat C^\downarrow} \\
& {\cat C}
\arrow[hook, from=1-1, to=1-3]
\arrow[from=1-1, to=2-2]
\arrow[from=1-3, to=2-2]
\end{tikzcd}\]

of monomorphisms in $\cat C$. Quotienting out by the relation that two monomorphisms shall be equal if and only if they factor through each other (necessarily through a monomorphism), we obtain the subobject fibration $\Sub(\cat C) \to \cat C$. The subobject fibration thus models the collection predicates on the objects of $\cat C$.

* Family fibration: Let $\cat B$ a category with pullbacks. Let $\Fam(P) : P \downarrow \cat B \to \cat B$ be the functor constructed as follows:

\[\begin{tikzcd}[sep=4ex]
{P\downarrow \cat B} && {\cat E} \\
{\cat B^\downarrow} && {\cat B} \\
\arrow[from=1-1, to=2-1]
\arrow["\dom", from=2-1, to=2-3]
\arrow[from=1-1, to=1-3]
\arrow["P", from=1-3, to=2-3]
\arrow["\cod", from=2-1, to=3-1]
\arrow["{\mathrm{Fam}(P)}"', curve={height=24pt}, from=1-1, to=3-1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-3]
\end{tikzcd}\]

We call $\Fam(P) : P \downarrow \cat B \to \cat B$ the family fibration of $P$. Indeed this is a fibration: any pullback of $P$ is a fibration, so is $\dom^*P$. Since $\cod$ is a fibration, as $\cat B$ has all pullbacks, then so is their composite $\cod \comp \dom^*P= \Fam(P)$. Objects in the fiber $(\Fam(P))^{-1}(I)$ are given by pairs $(f:X \to I, \alpha \in p^{-1}(X))$. In fact, if $P$ is an arbitrary functor, $\Fam(P)$ is always an opfibration, the free opfibration generated by $P$. Thus, $\Fam(P)$ is both a fibration and an opfibration. One can show that opcartesian transport serves as taking sums (or existential quantification), and that they commute with cartesian transport, serving as reindexing, in a canonical way (via the Beck–Chevalley isomorphisms). Hence, the family construction on a fibration $p$ can be understood as the result by freely adding sums to $p$, which are internally indexed, i.e., indexed by the base category $\cat B$. Accordingly, we also write $\Sigma(P) := \Fam(P)$.

One could replace $\dom$ in the above definition by a full subfibration of itself, corresponding to a version of the family construction that is the sum completion only w.r.t. a chosen class of morphisms om $\cat B$.

Let $P: \cat E \to \cat B$ be a fibration.
The vertical–cartesian factorization system $(\ver, \car)$ induced by $P$ on $\cat E$ is an orthogonal factorization system where

* the left class (vertical morphisms) is given by the maps projecting to isomorphisms and

* the right class (cartesian morphisms) is given by cartesian maps.

In practice, this means every arrow of $\cat E$ can be factored in a unique way as a vertical map followed by a cartesian one:

\begin{equation}
% https://q.uiver.app?q=WzAsMyxbMCwwLCJcXGNkb3QiXSxbNCwwLCJcXGNkb3QiXSxbMiwwLCJcXGNkb3QiXSxbMCwxLCJcXHZhcnBoaSIsMCx7ImN1cnZlIjotNX1dLFswLDIsIlxcdmFycGhpXlxcbmF0IiwyXSxbMiwxLCJcXHZhcnBoaV5cXGZsYXQiLDJdXQ==
\begin{tikzcd}[ampersand replacement=\&,sep=scriptsize]
\cdot \&\& \cdot \&\& \cdot
\arrow["\varphi", curve={height=-25pt}, dashed, from=1-1, to=1-5]
\arrow["{\varphi^\ver}"', from=1-1, to=1-3]
\arrow["{\varphi^\car}"', from=1-3, to=1-5]
\end{tikzcd}
\end{equation}

This factorization is manifest when we present $P$ as the Grothendieck construction of its fibers: in that case, morphisms in the total category are literally pairs $\lens{f^\ver}{f^\car}$ where $f^\car$ is cartesian and $f^\ver$ is vertical.

The most important property of this factorization system is the following:

Let $P:\cat E \to \cat B$ be a fibration. In $\cat E$, every cospan:

\begin{equation}
% https://q.uiver.app/#q=WzAsMyxbMSwwLCJcXGNkb3QiXSxbMCwxLCJcXGNkb3QiXSxbMSwxLCJcXGNkb3QiXSxbMCwyLCJcXHZlciJdLFsxLDIsIlxcY2FyIiwyXV0=
\begin{tikzcd}[ampersand replacement=\&]
\& \cdot \\
\cdot \& \cdot
\arrow["\ver", from=1-2, to=2-2]
\arrow["\car"', from=2-1, to=2-2]
\end{tikzcd}
\end{equation}

admits a pullback:

\begin{equation}
\label{eq:carversq}
% https://q.uiver.app/#q=WzAsNCxbMSwwLCJcXGNkb3QiXSxbMCwxLCJcXGNkb3QiXSxbMSwxLCJcXGNkb3QiXSxbMCwwLCJcXGNkb3QiXSxbMCwyLCJcXHZlciJdLFsxLDIsIlxcY2FyIiwyXSxbMywxLCJcXHZlciIsMl0sWzMsMCwiXFxjYXIiXSxbMywyLCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XV0=
\begin{tikzcd}[ampersand replacement=\&]
\cdot \& \cdot \\
\cdot \& \cdot
\arrow["\ver", from=1-2, to=2-2]
\arrow["\car"', from=2-1, to=2-2]
\arrow["\ver"', from=1-1, to=2-1]
\arrow["\car", from=1-1, to=1-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\end{tikzcd}
\end{equation}

Conversely, every square like (<ref>) is a pullback square.

Given a fibration $P : \cat E \to \cat B$, its dual (or fiberwise opposite) is another fibration $\dual P : \dual{\cat E} \to \cat B$ constructed as follows.

The category $\dual{\cat E}$ is the category that has the same objects as $\cat E$ and as morphisms equivalence classes of vertical-cartesian spans in $\cat E$, i.e. spans in $\cat E$ of the form

\begin{equation}
% https://q.uiver.app/?q=WzAsMyxbMCwxLCJYIl0sWzEsMCwiXFxjZG90ICJdLFsyLDEsIlkiXSxbMSwyLCJcXGNhciJdLFsxLDAsIlxcdmVyIiwyXV0=
\begin{tikzcd}[ampersand replacement=\&, sep=small]
\& {\cdot } \\
\cdot \&\& \cdot
\arrow["\car", from=1-2, to=2-3]
\arrow["\ver"', from=1-2, to=2-1]
\end{tikzcd}
\end{equation}

They compose because vertical arrows can always be pulled back against cartesian arrows:

\begin{equation}
% https://q.uiver.app/#q=WzAsNixbMCwyLCJYIl0sWzEsMSwiXFxjZG90ICJdLFsyLDIsIlkiXSxbMywxLCJcXGNkb3QiXSxbNCwyLCJaIl0sWzIsMCwiXFxjZG90Il0sWzEsMiwiXFxjYXIiLDAseyJsYWJlbF9wb3NpdGlvbiI6ODB9XSxbMSwwLCJcXHZlciIsMl0sWzMsMiwiXFx2ZXIiLDIseyJsYWJlbF9wb3NpdGlvbiI6MzB9XSxbMyw0LCJcXGNhciJdLFs1LDEsIlxcdmVyIiwyXSxbNSwzLCJcXGNhciJdLFs1LDIsIiIsMix7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dXQ==
\begin{tikzcd}[ampersand replacement=\&, sep=small]
\&\& \cdot \\
\& {\cdot } \&\&\cdot \\
X \&\& Y \&\& Z
\arrow["\car"{pos=0.8}, from=2-2, to=3-3]
\arrow["\ver"', from=2-2, to=3-1]
\arrow["\ver"'{pos=0.3}, from=2-4, to=3-3]
\arrow["\car", from=2-4, to=3-5]
\arrow["\ver"', from=1-3, to=2-2]
\arrow["\car", from=1-3, to=2-4]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=3-3]
\end{tikzcd}
\end{equation}

Hence this defines a category, and $P$ still works as a projection onto $\cat B$.

The fibration structure comes from noticing one can still lift arrows to cartesian arrows. More easily, since our fibrations are cloven, we can define

\begin{equation}
\dual P := \int (\de P \comp (-)^\op)
\end{equation}

which is a fibration by construction.
This point of view will be also useful later on.

The dual fibration construction extends to a functor $\dual{(-)} : \Fib(\cat B) \to \Fib(\cat B)$.

Recall a map of fibrations $F : P \to Q$ is a functor between the total spaces of $P$ and $Q$ that makes the obvious triangle commute and that respects the cartesian-vertical factorization system:

\begin{equation}
% https://q.uiver.app/?q=WzAsMyxbMiwwLCJcXEUiXSxbMSwxLCJcXEIiXSxbMCwwLCJcXEQiXSxbMiwwLCJmIl0sWzIsMSwicSIsMl0sWzAsMSwicCJdXQ==
\begin{tikzcd}[ampersand replacement=\&, sep=small]
\cat D \&\& \cat E \\
\& \cat B
\arrow["F", from=1-1, to=1-3]
\arrow["Q"', from=1-1, to=2-2]
\arrow["P", from=1-3, to=2-2]
\end{tikzcd}
\end{equation}

Explicitly, it means $F$ sends cartesian arrows to cartesian arrows.
This is equivalent to say $F$ defines functors between the fibers of $P$ and $Q$: for a given $B \in \cat B$, $\de F_B : \de P(B) \to \de Q(B)$ is a well-defined functor mapping $P$-vertical arrows over $B$ to $Q$-vertical arrows over $B$, and such that for every arrow $f : B' \to B$ in $\cat B$, the following square commutes:

\begin{equation}
% https://q.uiver.app?q=WzAsNCxbMCwwLCJcXGRlIFAoQikiXSxbMSwwLCJcXGRlIFEoQikiXSxbMCwxLCJcXGRlIFAoQicpIl0sWzEsMSwiXFxkZSBRKEInKSJdLFswLDEsIlxcZGUgRl9CIl0sWzIsMywiXFxkZSBGX3tCJ30iXSxbMCwyLCJcXGRlIFAoZikiLDJdLFsxLDMsIlxcZGUgUShmKSJdXQ==
\begin{tikzcd}[ampersand replacement=\&]
{\de P(B)} \& {\de Q(B)} \\
{\de P(B')} \& {\de Q(B')}
\arrow["{\de F_B}", from=1-1, to=1-2]
\arrow["{\de F_{B'}}", from=2-1, to=2-2]
\arrow["{\de P(f)}"', from=1-1, to=2-1]
\arrow["{\de Q(f)}", from=1-2, to=2-2]
\end{tikzcd}
\end{equation}

Now if we take the fiberwise opposites of $P$ and $Q$, we can still define $\dual F$ by applying $F$ to both legs of the spans. Since $F$ respects the cartesian factorization systems of the fibrations, the image span is still of the required form.

§ LENSES AND DIALECTICA

§.§ Lenses

In their most essential form, lenses are just morphisms in a dualized fibration.
Originally, the name lenses referred to morphisms in the dual of the simple fibration, so that $\Lens(\cat C) := \dual{\cat C^\proj}$, where $\cat C$ is a category with products.

\begin{equation}
% https://q.uiver.app?q=WzAsNixbMSwxLCJVIl0sWzIsMSwiViJdLFsyLDAsIlYgXFx0aW1lcyBZIl0sWzAsMSwiVSJdLFswLDAsIlUgXFx0aW1lcyBYIl0sWzEsMCwiVSBcXHRpbWVzIFkiXSxbMCwxLCJmIiwwLHsiY29sb3VyIjpbMCw2MCw2MF19LFswLDYwLDYwLDFdXSxbMiwxLCJcXHBpX1YiLDJdLFszLDAsIiIsMCx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzUsMiwiZiBcXHRpbWVzIFkiXSxbNSwxLCIiLDAseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XSxbNSwwLCJcXHBpX1UiLDJdLFs0LDMsIlxccGlfVSIsMl0sWzUsNCwiZl5cXHNoYXJwIiwyLHsiY29sb3VyIjpbMCw2MCw2MF19LFswLDYwLDYwLDFdXV0=
\begin{tikzcd}[ampersand replacement=\&]
{U \times X} \& {U \times Y} \& {V \times Y} \\
U \& U \& V
\arrow["f", from=2-2, to=2-3]
\arrow["{\pi_V}"', from=1-3, to=2-3]
\arrow[Rightarrow, no head, from=2-1, to=2-2]
\arrow["{f \times Y}", from=1-2, to=1-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
\arrow["{\pi_U}"', from=1-2, to=2-2]
\arrow["{\pi_U}"', from=1-1, to=2-1]
\arrow["{f^\sharp}"', from=1-2, to=1-1]
\end{tikzcd}
\end{equation}

In <cit.>, Spivak shows the name lenses deserves to be applied to much more general morphisms. Chiefly, dependent lenses are morphisms in the dual of the codomain fibration of a category with products, but examples abound:

\begin{equation}
% https://q.uiver.app?q=WzAsNixbMSwxLCJVIl0sWzIsMSwiViJdLFsyLDAsIlkiXSxbMCwxLCJVIl0sWzAsMCwiWCJdLFsxLDAsIlUgXFx0aW1lc19WIFkiXSxbMCwxLCJmIiwwLHsiY29sb3VyIjpbMCw2MCw2MF19LFswLDYwLDYwLDFdXSxbMiwxXSxbMywwLCIiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs1LDIsImZfWSJdLFs1LDEsIiIsMCx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs1LDBdLFs0LDNdLFs1LDQsImZeXFxzaGFycCIsMix7ImNvbG91ciI6WzAsNjAsNjBdfSxbMCw2MCw2MCwxXV1d
\begin{tikzcd}[ampersand replacement=\&]
X \& {U \times_V Y} \& Y \\
U \& U \& V
\arrow["f", from=2-2, to=2-3]
\arrow[from=1-3, to=2-3]
\arrow[Rightarrow, no head, from=2-1, to=2-2]
\arrow["{f_Y}", from=1-2, to=1-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
\arrow[from=1-2, to=2-2]
\arrow[from=1-1, to=2-1]
\arrow["{f^\sharp}"', from=1-2, to=1-1]
\end{tikzcd}
\end{equation}

Let $P: \cat E \to \cat B$ be a fibration.
Its dual fibration $\dual P: \dual{\cat E} \to \cat B$ is called the fibration of $P$-lenses, and morphisms in $\dual{\cat E}$ are $P$-lenses.

One might ask why are lenses defined like this. The answers can be many. For instance, suppose we want to represent a dialogue between two parties, given in Q&A style. Then we are led naturally to the definition of $P$-lens.

In fact we first look at what types we have around in this situation. Our first agent, let's call it Alice, will choose among a bunch of things she knows (her `state', for lack of a better word), and use them to produce a question for Bob, our second agent. This is the forward part (or `cartesian' part, if we look at fibrations).
Now, how does a reply look like? Well, first of all a reply to a question $v \in V$ is going to be a member of a plethora of possible replies $Y(v)$, i.e. a term of a dependent type over $V$. This motivates the use of a fibration to represent different levels of a conversation: answers depend on questions.
Secondly, the answer Bob will give will produce a change in the state of Alice, which is itself a dependent type, and the entire conversation will happen with such state `in context'. This reply mechanics is represented by the backward (or `vertical' part).

More accurately, a $P$-lens represents a party engaging in a dialogue, or better an interface between two dialoguing parties. In fact, a $P$-lens represents a policy to turn questions to questions and answers to answers. A $P$-lens with a trivial left boundary (sometimes called a state) represents a questioning party, whereas a $P$-lens with a trivial right boundary (sometimes called a costate) represents an answering party.

This perspective is explored in the seminal work <cit.>.

§.§ Dialectica categories

Dialectica categories are made of morphisms very similar to lenses, and also have a formal essence which is very simple to capture with very little structure. For the categories we are presenting in due course, we are employing type-theoretic notation.

The Dialectica category $D\cat C$ has

* as objects, triples

\begin{equation}
(U : \cat C, X : \cat C, \alpha : \Sub(U \times X))
\end{equation}

* as morphisms $(U,X,\alpha) \to (V,Y,\beta)$, triples

f: U →V,

f^♯: U ×Y →X,

∀u:U, y:Y,   α(u, f^♯(u, y)) ⊆β(f(u), y)

Hence $D\cat C$ is a category of lenses `augmented with predicates'.

Can $D\cat C$ be constructed in a similar way to $\Lens(\cat C)$?
Can its shape be abstracted, like we did for $p$-lenses?

§ DIALENSES AS A COMMON FRAMEWORK

§.§ Iterated fibrations and their duals

The data needed to construct a Dialectica category is easily seen to amount to an iterated fibration:

\begin{equation}
% https://q.uiver.app?q=WzAsNixbMCwwLCJcXGNhdCBQIl0sWzAsMSwiXFxjYXQgRSJdLFswLDIsIlxcY2F0IEMiXSxbMSwyLCJmOlUgXFx0byBWIl0sWzEsMSwiZl5cXHNoYXJwOiBmXipZIFxcdG8gWCJdLFsxLDAsImZeXFxkb3VibGVzaGFycCA6IChmXlxcc2hhcnApXipcXGFscGhhIFxcdG8gZl4qXFxiZXRhIl0sWzEsMiwicCIsMl0sWzAsMSwicSIsMl1d
\begin{tikzcd}[ampersand replacement=\&]
{\cat P} \& {`\alpha \subseteq \beta'} \\
{\cat E} \& {f^\sharp: f^*Y \to X} \\
{\cat C} \& {f:U \to V}
\arrow["P"', from=2-1, to=3-1]
\arrow["Q"', from=1-1, to=2-1]
\end{tikzcd}
\end{equation}

Thus we can wonder if somehow the simple construction producing $P$-lenses from $P$ extends to the extra data of $Q$.

First, notice such an iterated fibration can be seen as exhibiting $Q$ as a morphism of fibrations over $\cat C$:

\begin{equation}
% https://q.uiver.app?q=WzAsMyxbMCwwLCJcXGNhdCBQIl0sWzIsMCwiXFxjYXQgRSJdLFsxLDEsIlxcY2F0IEMiXSxbMSwyLCJwIl0sWzAsMSwicSJdLFswLDIsInEgXFxjb21wIHAiLDJdXQ==
\begin{tikzcd}[ampersand replacement=\&]
{\cat P} \&\& {\cat E} \\
\& {\cat C}
\arrow["P", from=1-3, to=2-2]
\arrow["Q", from=1-1, to=1-3]
\arrow["{Q \comp P}"', from=1-1, to=2-2]
\end{tikzcd}
\end{equation}

In fact the triangle trivially commutes and $Q$ respects cartesian arrows since the cartesian arrows of $\cat P$ as a category fibered over $\cat C$ are exactly the cartesian arrows of $\cat P$ (as a category fibered over $\cat E$) which are over cartesian arrows of $\cat E$.

Something stronger is true: $Q$ is actually a fibration of fibrations, i.e. a `fiberwise fibration', since Bénaboú showed that fibrations in $\Fib(\cat C)$ are given by maps of fibrations which are themselves fibrations.
A published account of this fact can be found in <cit.>.

Then, since $\dual{(-)}$ is a functorial construction $\Fib(\cat C) \to \Fib(\cat C)$, it can be applied to the whole triangle:

\begin{equation}
% https://q.uiver.app?q=WzAsMyxbMCwwLCJcXGNhdCBQIl0sWzIsMCwiXFxjYXQgRSJdLFsxLDEsIlxcY2F0IEMiXSxbMSwyLCJwIl0sWzAsMSwicSJdLFswLDIsInEgXFxjb21wIHAiLDJdXQ==
\begin{tikzcd}[ampersand replacement=\&]
{\dual{\cat P}} \&\& {\dual{\cat E}} \\
\& {\cat C}
\arrow["\dual P", from=1-3, to=2-2]
\arrow["\dual Q", from=1-1, to=1-3]
\arrow["\dual {(Q \comp P)}"', from=1-1, to=2-2]
\end{tikzcd}
\end{equation}

To understand how $\dual{\cat P}$ looks like now, we need to stop for a moment and understand the factorization systems at play in this situation.

Remember $P$ induces a factorization system on $\cat E$ which $\dual{\cat E}$ inherits as ($P$-vertical$^\op$, $P$-cartesian) (also denoted as $(\ver_P^\op, \car_P)$).
On $\cat P$ we have a more refined factorization system, since we have three kinds of arrows:

* $Q$-cartesian arrows, which are cartesian lifts of $\cat E$-arrows, and come in two subcategories:

* $P$-cartesian arrows, which are cartesian lifts of $\cat C$-arrows, hence cartesian $\cat E$-arrows,

* $P$-vertical arrows, which are cartesian lifts of vertical $\cat E$-arrows,

* $Q$-vertical arrows, which are in the fibers of $P$.

This forms a ternary factorization system ($Q$-vertical, $P$-vertical, $P$-cartesian), or $(\ver_Q, \ver_P, \car_P)$, which means every arrow $\varphi$ in $\cat P$ factors in three parts:

\begin{equation}
% https://q.uiver.app?q=WzAsNCxbNCwwLCJcXGNkb3QiXSxbMiwwLCJcXGNkb3QiXSxbNiwwLCJcXGNkb3QiXSxbMCwwLCJcXGNkb3QiXSxbMywxLCJcXHZhcnBoaV57XFx2ZXJfUX0iLDJdLFsxLDAsIlxcdmFycGhpXntcXHZlcl9QfSIsMl0sWzAsMiwiXFx2YXJwaGlee1xcY2FyX1B9IiwyXSxbMywyLCJcXHZhcnBoaSIsMSx7ImN1cnZlIjotNSwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoiZGFzaGVkIn19fV0sWzEsMiwiXFx2YXJwaGlee1xcY2FyX1F9IiwxLHsiY3VydmUiOi0zLCJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XV0=
\begin{tikzcd}[ampersand replacement=\&,sep=scriptsize]
\cdot \&\& \cdot \&\& \cdot \&\& \cdot
\arrow["{\varphi^{\ver_Q}}"', from=1-1, to=1-3]
\arrow["{\varphi^{\ver_P}}"', from=1-3, to=1-5]
\arrow["{\varphi^{\car_P}}"', from=1-5, to=1-7]
\arrow["\varphi"{description}, curve={height=-50pt}, dashed, from=1-1, to=1-7]
\arrow["{\varphi^{\car_Q}}"{description}, curve={height=-25pt}, dashed, from=1-3, to=1-7]
\end{tikzcd}
\end{equation}

When we turn around the fibers of $\cat E$, we end up swapping $Q$-vertical and $P$-vertical arrows:

\begin{equation}
% https://q.uiver.app/#q=WzAsNCxbNCwwLCJcXGNkb3QiXSxbMiwwLCJcXGNkb3QiXSxbNiwwLCJcXGNkb3QiXSxbMCwwLCJcXGNkb3QiXSxbMSwzLCJcXHZhcnBoaV57XFx2ZXJfUX0iXSxbMCwxLCJcXHZhcnBoaV57XFx2ZXJfUH0iXSxbMCwyLCJcXHZhcnBoaV57XFxjYXJfUH0iLDJdLFszLDIsIlxcdmFycGhpIiwxLHsiY3VydmUiOi01fV1d
\begin{tikzcd}[ampersand replacement=\&,sep=scriptsize]
\cdot \&\& \cdot \&\& \cdot \&\& \cdot
\arrow["{\varphi^{\ver_Q}}", from=1-3, to=1-1]
\arrow["{\varphi^{\ver_P}}", from=1-5, to=1-3]
\arrow["{\varphi^{\car_P}}"', from=1-5, to=1-7]
\arrow["\varphi"{description}, curve={height=-30pt}, dashed, from=1-1, to=1-7]
\end{tikzcd}
\end{equation}

Hence on $\dual{\cat P}$ we end up with a ternary factorization system ($P$-vertical$^\op$, $Q$-vertical$^\op$, $P$-cartesian), i.e. where $P$- and $Q$-vertical arrows are swapped (both as arrows and as classes in the ternary factorization system).

We can understand this factorization system as an ambifibration[The definition and name of ambifibration seems to be due to Kock and Joyal, but unpublished. See <cit.>.] structure on $\dual Q$:

Let $(L, R)$ be a factorization system on $\cat E$. An ambifibration $A : \cat P \to \cat E$ is a functor such that

* every arrow in $L$ has an opcartesian lift ($A$ restrics to an opfibration on $L$)

* every arrow in $R$ has a cartesian lift ($A$ restrics to a fibration on $R$)

This induces the ternary factorization system (opcartesian, vertical, cartesian) on $\cat P$:

\begin{equation}
% file:///home/jsb20179/data/software/quiver/src/index.html?q=WzAsMTAsWzMsMSwiQiJdLFs0LDEsIkMiXSxbMSwxLCJBIl0sWzIsMSwiQiJdLFs0LDAsIkMnIl0sWzEsMCwiQSciXSxbMiwwLCJcXGVsbF8qIEEnIl0sWzMsMCwicl4qQyciXSxbMCwwLCJcXGNhdCBGIl0sWzAsMSwiXFxjYXQgRCJdLFswLDEsIlxcaW4gUiIsMl0sWzIsMywiXFxpbiBMIiwyXSxbMywwLCIiLDIseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs1LDYsIlxcb3BjYXIiLDJdLFs3LDQsIlxcY2FyIiwyXSxbNiw3LCJcXGluIFYiLDJdLFs4LDksImEiLDJdXQ==
\begin{tikzcd}[ampersand replacement=\&]
{\cat P} \& {A'} \& {\ell_* A'} \& {r^*C'} \& {C'} \\
{\cat E} \& A \& B \& B \& C
\arrow["{r \in R}"', from=2-4, to=2-5]
\arrow["{\ell \in L}"', from=2-2, to=2-3]
\arrow[Rightarrow, no head, from=2-3, to=2-4]
\arrow["\opcar"', from=1-2, to=1-3]
\arrow["\car"', from=1-4, to=1-5]
\arrow["\ver"', from=1-3, to=1-4]
\arrow["A"', from=1-1, to=2-1]
\end{tikzcd}
\end{equation}

Looking at the iterated fibration $\dual{\cat P} \nto{\dual Q} \dual{\cat E} \nto{\dual P} \cat C$, we see:

* $\dual{\cat E}$ has the factorization system ($P$-vertical$^\op$, $P$-cartesian),

* $\dual Q$ is a fibration on the cartesian class of $\cat E$, given by $Q$, and became an opfibration on the vertical class since it acts like $\dual{Q}$ there.
Hence $\dual{Q}$ is an ambifibration over $\dual{\cat E}$ with respect to the factorization system $(\ver^\op, \car)$.

This is very close to what we are looking for: the data of a morphism in Dialectica is indeed that of a triple of morphisms, except the last one (first in the factorization) needs to point in the same direction as the first one (last in the factorization).
This suggests a last dualization is needed, involving only the fibration $Q$.

At this point, it's a good idea to introduce some new notation and terminology.
First of all, let us make the notation $\dual{p} : \dual{\cat E} \to \cat B$ more precise by specifying the base with respect to which we are taking the dual:

\begin{equation}
\dual[\cat B]{p} : \dual[\cat B]{\cat E} \to \cat B.
\end{equation}

Moreover, we introduce the following construction:

Let $\mathbf{P} = (\cat E_n \nlongto{P_n} \cdots \longto \cat E_2 \nlongto{P_2} \cat E_1 \nlongto{P_1} \cat B)$ be a sequence of $n$ fibrations (an $n$-fold fibration).
The iterated dual of $\mathbf P$ is defined inductively on its length as follows:

* $n=1$

\begin{equation}
\dual[1]{(\cat E_1 \nlongto{P_1} \cat E_0)} = \dual[\cat E_0]{\cat E_1} \nlongto{\dual[\cat E_0]{P_1}} \cat E_0
\end{equation}

* $n=k+1$

\begin{equation}
\dual[k+1]{(\cat E_{k+1} \nlongto{P_{k+1}} \cdots \nlongto{P_2} \cat E_1 \nlongto{P_1} \cat E_0)}
\dual[k]{\dual[\cat E_0]{(\cat E_{k+1} \nlongto{P_{k+1}} \cdots \cat E_1)}} \nlongto{\dual[\cat E_0]{P_1}} \cat E_0
\end{equation}

Suppose $P:\cat E \to \cat C$ is actually a comprehension category <cit.>, thus we have also a functor $\{-\}:\cat E \to \cat C$.
This can be seen as a way to cast a dependent type into a simple one.
By repeatedly pulling back $P$ along $\{-\}$ we can form towers of fibrations of arbitrary height.

§.§ Dialenses

Let's see the result of an iterated dual of length $2$, i.e. $\dual[2]{(\cat E_2 \nto{P_2} \cat E_1 \nto{P_1} \cat E_0)}$.
Below are unpacked the various bits the morphisms in $\dual[\cat E_1]{\dual[\cat E_0]{\cat E_2}}$ are made of: as you can see we end up with a ternary factorization corresponding to three changes in directions as we go up the sequence of fibrations:

\begin{equation}
% file:///home/jsb20179/data/software/quiver/src/index.html?q=WzAsMTUsWzMsNCwiVSJdLFs0LDQsIlYiXSxbMCw0LCJcXGNhdCBDIl0sWzAsMiwiXFxkdWFsW1xcY2F0IENde1xcY2F0IEVfMX0iXSxbNCwyLCJZIl0sWzMsMiwiZl4qWSJdLFsxLDQsIlUiXSxbMiw0LCJVIl0sWzIsMiwiZl4qWSJdLFsxLDIsIlgiXSxbMCwwLCJcXGR1YWxbXFxjYXQgRV8xXXtcXGR1YWxbXFxjYXQgQ117XFxjYXQgRV8yfX0iXSxbMSwwLCJcXGFscGhhIl0sWzQsMCwiXFxiZXRhIl0sWzIsMCwiKGZeXFxzaGFycCleKlxcYWxwaGEiXSxbMywwLCJmXipcXGJldGEiXSxbMCwxLCJmIiwwLHsiY29sb3VyIjpbMCw2MCw2MF19LFswLDYwLDYwLDFdXSxbNSw0LCJmX1kiXSxbNiw3LCIiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs3LDAsIiIsMCx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzgsOSwiZl5cXHNoYXJwIiwyLHsiY29sb3VyIjpbMCw2MCw2MF19LFswLDYwLDYwLDFdXSxbOCw1LCIiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFszLDIsIlxcZHVhbFtcXGNhdCBDXXtwXzF9IiwyXSxbMTAsMywiXFxkdWFsW1xcY2F0IEVfMV17XFxkdWFsW1xcY2F0IENde3BfMn19IiwyXSxbMTQsMTIsImZfXFxiZXRhIl0sWzEzLDExLCJmXlxcc2hhcnBfXFxhbHBoYSIsMl0sWzEzLDE0LCJmXlxcZG91Ymxlc2hhcnAiLDAseyJjb2xvdXIiOlswLDYwLDYwXX0sWzAsNjAsNjAsMV1dXQ==
\begin{tikzcd}[ampersand replacement=\&, sep=scriptsize]
{\dual[\cat E_1]{\dual[\cat E_0]{\cat E_2}}} \& \alpha \& {(f^\sharp)^*\alpha} \& {f^*\beta} \& \beta \\
\\
{\dual[\cat E_0]{\cat E_1}} \& X \& {f^*Y} \& {f^*Y} \& Y \\
\\
{\cat E_0} \& U \& U \& U \& V
\arrow["f", color={red}, from=5-4, to=5-5]
\arrow["{f_Y}", from=3-4, to=3-5]
\arrow[Rightarrow, no head, from=5-2, to=5-3]
\arrow[Rightarrow, no head, from=5-3, to=5-4]
\arrow["{f^\sharp}"', color={red}, from=3-3, to=3-2]
\arrow[Rightarrow, no head, from=3-3, to=3-4]
\arrow["{\dual[\cat E_0]{P_1}}"', from=3-1, to=5-1]
\arrow["{\dual[\cat E_1]{\dual[\cat E_0]{P_2}}}"', from=1-1, to=3-1]
\arrow["{f_\beta}", from=1-4, to=1-5]
\arrow["{f^\sharp_\alpha}"', from=1-3, to=1-2]
\arrow["{f^\doublesharp}", color={red}, from=1-3, to=1-4]
\end{tikzcd}
\end{equation}

To see this reproduces <ref>, let's unpack this situation when $P_2 = \cod:\cat C_\proj^\downarrow \to \cat C$ and $P_1$ is the fibration of monos of the domain over $\cat C_\proj^\downarrow$, that is, the fiber over $\pi_U : U \times X \to U$ is given by the subobjects of $U \times X$:

\begin{equation}
% file:///home/jsb20179/data/software/quiver/src/index.html?q=WzAsMTUsWzIsMiwiWCJdLFszLDIsIlgiXSxbNCwyLCJYIixbMCw2MCw2MCwxXV0sWzUsMiwiWSIsWzAsNjAsNjAsMV1dLFs1LDEsIlYgXFx0aW1lcyBZIl0sWzQsMSwiViBcXHRpbWVzIFgiXSxbNSwwLCJcXGJldGEiXSxbMiwwLCJcXGFscGhhIl0sWzIsMSwiVSBcXHRpbWVzIFgiLFswLDYwLDYwLDFdXSxbMywxLCJWIFxcdGltZXMgWCIsWzAsNjAsNjAsMV1dLFszLDAsIihmXlxcc2hhcnApXipcXGFscGhhIixbMCw2MCw2MCwxXV0sWzQsMCwiZl4qXFxiZXRhIixbMCw2MCw2MCwxXV0sWzAsMiwiXFxjYXQgQyJdLFswLDEsIlxcY2F0IENeXFxkb3duYXJyb3dfXFxwcm9qIl0sWzAsMCwiXFxjYXQgUCJdLFswLDEsIiIsMix7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzEsMiwiIiwyLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbMiwzLCJmIiwyLHsiY29sb3VyIjpbMCw2MCw2MF19LFswLDYwLDYwLDFdXSxbNSw0LCJmX1YiXSxbNCwzXSxbNSwyXSxbNSwzLCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XSxbOSw1LCIiLDIseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs5LDgsImZeXFxzaGFycCIsMix7ImNvbG91ciI6WzAsNjAsNjBdfSxbMCw2MCw2MCwxXV0sWzExLDYsImZfe1xcYmV0YX0iXSxbMTAsNywiZl5cXHNoYXJwX1xcYWxwaGEiLDJdLFsxMCwxMSwiZl5cXGRvdWJsZXNoYXJwIiwwLHsiY29sb3VyIjpbMCw2MCw2MF0sInN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1vbm8ifX19LFswLDYwLDYwLDFdXSxbNyw4LCIiLDEseyJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtb25vIn19fV0sWzEwLDksIiIsMSx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1vbm8ifX19XSxbMTEsNSwiIiwxLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibW9ubyJ9fX1dLFs2LDQsIiIsMSx7InN0eWxlIjp7InRhaWwiOnsibmFtZSI6Im1vbm8ifX19XSxbOSwxXSxbOCwwXSxbMTEsNCwiIiwyLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV0sWzEwLDgsIiIsMix7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFsxNCwxMywiUSJdLFsxMywxMiwiUCJdXQ==
\begin{tikzcd}[ampersand replacement=\&]
{\dual[\cat C^\downarrow_\proj]{\dual[\cat C]{\cat P}}} \&[-2ex]\&[-2ex] \alpha \& \textcolor{rgb,255:red,214;green,92;blue,92}{(f^\sharp)^*\alpha} \& \textcolor{rgb,255:red,214;green,92;blue,92}{f^*\beta} \& \beta \\
{\cat C^\downarrow_\proj} \&\& \textcolor{rgb,255:red,214;green,92;blue,92}{U \times X} \& \textcolor{rgb,255:red,214;green,92;blue,92}{V \times X} \& {V \times X} \& {V \times Y} \\
{\dual[\cat C]{\cat C}} \&\& X \& X \& \textcolor{rgb,255:red,214;green,92;blue,92}{X} \& \textcolor{rgb,255:red,214;green,92;blue,92}{Y}
\arrow[Rightarrow, no head, from=3-3, to=3-4]
\arrow[Rightarrow, no head, from=3-4, to=3-5]
\arrow["f"', color={rgb,255:red,214;green,92;blue,92}, from=3-5, to=3-6]
\arrow["{f_V}", from=2-5, to=2-6]
\arrow[from=2-6, to=3-6]
\arrow[from=2-5, to=3-5]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-5, to=3-6]
\arrow[Rightarrow, no head, from=2-4, to=2-5]
\arrow["{f^\sharp}"', color={rgb,255:red,214;green,92;blue,92}, from=2-4, to=2-3]
\arrow["{f_{\beta}}", from=1-5, to=1-6]
\arrow["{f^\sharp_\alpha}"', from=1-4, to=1-3]
\arrow["{f^\doublesharp}", color={rgb,255:red,214;green,92;blue,92}, tail, from=1-4, to=1-5]
\arrow[tail, from=1-3, to=2-3]
\arrow[tail, from=1-4, to=2-4]
\arrow[tail, from=1-5, to=2-5]
\arrow[tail, from=1-6, to=2-6]
\arrow[from=2-4, to=3-4]
\arrow[from=2-3, to=3-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-5, to=2-6]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-90}, draw=none, from=1-4, to=2-3]
\arrow["{\dual[\cat C^\downarrow_\proj]{\dual[\cat C]{P_2}}}", from=1-1, to=2-1]
\arrow["{\dual[\cat C]{P_1}}", from=2-1, to=3-1]
\end{tikzcd}
\end{equation}

Notice the sequence of fibrations we used here is obtained quite naturally as a coproduct completion:

\begin{equation}
\begin{tikzcd}[ampersand replacement=\&,sep=5ex, column sep=3ex]
{\cat C^\subseteq \times_{\cat C} \cat C_\proj^\downarrow} \& {\Sub(\cat C)} \\
{\cat C_\proj^\downarrow} \& {\cat C} \\
{\cat C}
\arrow["{\sf sub}", from=1-2, to=2-2]
\arrow["\times", from=2-1, to=2-2]
\arrow["{\cod = P_1}"', from=2-1, to=3-1]
\arrow[from=1-1, to=1-2]
\arrow["{P_2}"', from=1-1, to=2-1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\end{tikzcd}
\end{equation}

Thus what we called `$\cat P$' above is really $\cat C^\subseteq \times_{\cat C} \cat C_\proj^\downarrow$.

Let $\mathbf{P}$ be a sequence of fibrations of length $n$. Its iterated dual $\dual[n]{\mathbf P}$ is called the iterated fibration of $\mathbf P$-dialenses.

Clearly dialenses of height $1$ are just $P$-lenses (<ref>) and Dialectica (<ref>) is a category of dialenses of height $2$.

The motivation for lenses given in <ref> generalizes naturally to dialenses of higher type. In fact, these can be seen to represent longer dialogues where at each stage, agents remember the previous ones.

Optics are a generalization of lenses introduced by the functional programming community to generalize the way lenses allow to access data to data structures other than record types (see <cit.>).
To do so, optics turn the `residual', which is that extra argument the backwards part of a lens has, into a first-class object which is explicitly `written' in the forward part and `read' in the backward part.
An optic $(A,B) \to (S,T)$ is comprised of a view $f:A \to M \bullet S$ and an update $f^\sharp : M \circ T \to B$, where $M$ is the residual. Here $A$ and $S$ belong to the same category $\cat C$, with $\bullet : \cat M \times \cat C \to \cat C$ being an action of the monoidal category $\cat M$, where $M$ lives instead. In turn $B$ and $T$ live in a possibly different category $\cat D$ also receiving an action $\circ$ of $\cat M$.
Finally, optics are quotiented by an equivalence relation that allows morphisms to `slide' across the residual, expressing the intuitive fact that computing something from some inputs and then save it in memory is equivalent to saving in memory the inputs and then later computing from those.

By varying the various pieces of data, optics can express a plethora of data accessing patterns. For a survey and more detailed definitions, we direct the reader to <cit.>.

We describe now how optics can be constructed as dialenses of height $2$, if of a bizarre kind.
First, recall from <cit.> that every (strict, for simplicity) action $\bullet : \cat M \times \cat C \to \cat C$ of a monoidal category $\cat M$ on a category $\cat C$ can be repackaged as a 2-opfibration $\Para(\bullet) \to B\cat M$, where $\Para(\bullet)$ is the bicategory of $\cat M$-parametric $\cat C$-morphisms (see <cit.>) and the projection to $B\cat M$ is given by projection out the parameter of a morphism.
Here let's ignore the two-dimensional information and just consider this as an opfibration. Opcartesian lifts are constructed as follows:

\begin{equation}
% file:///home/jsb20179/data/software/quiver/src/index.html?q=WzAsNixbMCwwLCJcXFBhcmEoXFxidWxsZXQpIl0sWzAsMSwiQlxcY2F0IE0iXSxbMSwxLCJcXGFzdCJdLFsyLDEsIlxcYXN0Il0sWzEsMCwiWCJdLFsyLDAsIm0gXFxidWxsZXQgWCJdLFswLDEsIlAiLDJdLFsyLDMsIm0iLDJdLFs0LDUsIihtLCAxX3ttIFxcYnVsbGV0IFh9KSJdLFs1LDIsIikiLDMseyJsYWJlbF9wb3NpdGlvbiI6MCwic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d
\begin{tikzcd}[ampersand replacement=\&]
{\Para(\bullet)} \& X \& {m \bullet X} \\
{B\cat M} \& \ast \& \ast
\arrow["P_\bullet"', from=1-1, to=2-1]
\arrow["m"', from=2-2, to=2-3]
\arrow["{(m, 1_{m \bullet X})}", from=1-2, to=1-3]
\end{tikzcd}
\end{equation}

Further on, we'll abbreviate $(m, 1_{m \bullet X})$ with $m_X$.

Then given two left $\cat M$-actegories $(\cat C,\bullet)$ and $(\cat D, \circ)$, one can construct the following tower of opfibrations:

\begin{equation}
% file:///home/jsb20179/data/software/quiver/src/index.html?q=WzAsNSxbMCwwLCJcXFBhcmEoXFxjaXJjKSBcXHRpbWVzX3tcXGNhdCBCTX0gXFxQYXJhKFxcYnVsbGV0KSJdLFswLDEsIlxcUGFyYShcXGJ1bGxldCkiXSxbMCwyLCJcXGNhdCBCTSJdLFsxLDEsIlxcY2F0IEJNIl0sWzEsMCwiXFxQYXJhKFxcY2lyYykiXSxbNCwzLCJcXGludCBcXGNpcmMiXSxbMSwzLCJcXGludCBcXGJ1bGxldCJdLFsxLDIsInBfMSA9IFxcaW50IFxcYnVsbGV0IiwyXSxbMCw0XSxbMCwxLCJwXzIiLDJdLFswLDMsIiIsMCx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dXQ==
\begin{tikzcd}[ampersand replacement=\&, sep=5ex]
{\Para(\circ) \times_{B \cat M} \Para(\bullet)} \& {\Para(\circ)} \\
{\Para(\bullet)} \& {B \cat M} \\
{B\cat M}
\arrow["{P_\circ}", from=1-2, to=2-2]
\arrow["{P_\bullet}", from=2-1, to=2-2]
\arrow["{P_\bullet}"', from=2-1, to=3-1]
\arrow[from=1-1, to=1-2]
\arrow["{P_\circ}"', from=1-1, to=2-1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=2-2]
\end{tikzcd}
\end{equation}

Its iterated dual produces mixed optics, up to the quotient on slidings (which can be seen as a result of coarse-graining the 2-dimensional data, see <cit.>):

\begin{equation}
% file:///home/jsb20179/data/software/quiver/src/index.html?q=WzAsMTUsWzEsMiwiXFxhc3QiLFswLDYwLDYwLDFdXSxbMiwyLCJcXGFzdCIsWzAsNjAsNjAsMV1dLFszLDIsIlxcYXN0Il0sWzQsMiwiXFxhc3QiXSxbMSwxLCJYIl0sWzIsMSwibSBcXGJ1bGxldCBYIl0sWzMsMSwibSBcXGJ1bGxldCBYIixbMCw2MCw2MCwxXV0sWzQsMSwiWSIsWzAsNjAsNjAsMV1dLFs0LDAsIlYiXSxbMywwLCJWIixbMCw2MCw2MCwxXV0sWzEsMCwiVSJdLFsyLDAsIm0gXFxjaXJjIFUiLFswLDYwLDYwLDFdXSxbMCwyLCJCXFxjYXQgTSJdLFswLDEsIlxcZHVhbFtCXFxjYXQgTV17XFxQYXJhKFxcYnVsbGV0KX0iXSxbMCwwLCJcXE9wdGljX3tcXGNhdCBNfShcXGJ1bGxldCwgXFxjaXJjKSJdLFswLDEsIm0iLDAseyJjb2xvdXIiOlswLDYwLDYwXX0sWzAsNjAsNjAsMV1dLFsxLDIsIiIsMCx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzIsMywiIiwwLHsibGV2ZWwiOjIsInN0eWxlIjp7ImhlYWQiOnsibmFtZSI6Im5vbmUifX19XSxbNCw1LCJtX1giXSxbNSw2LCIiLDAseyJsZXZlbCI6Miwic3R5bGUiOnsiaGVhZCI6eyJuYW1lIjoibm9uZSJ9fX1dLFs3LDYsImYiLDIseyJjb2xvdXIiOlswLDYwLDYwXX0sWzAsNjAsNjAsMV1dLFs5LDgsIjFfViIsMCx7ImxldmVsIjoyLCJzdHlsZSI6eyJoZWFkIjp7Im5hbWUiOiJub25lIn19fV0sWzEwLDExLCJtX1UiXSxbMTEsOSwiZl5cXHNoYXJwIiwwLHsiY29sb3VyIjpbMCw2MCw2MF19LFswLDYwLDYwLDFdXSxbMTMsMTIsIlxcZHVhbFtCXFxjYXQgTV17UF9cXGJ1bGxldH0iXSxbMTQsMTMsIlxcdmlldyJdXQ==
\begin{tikzcd}[ampersand replacement=\&]
{\Optic_{\cat M}(\bullet, \circ)} \& U \& \textcolor{rgb,255:red,214;green,92;blue,92}{m \circ U} \& \textcolor{rgb,255:red,214;green,92;blue,92}{V} \& V \\
{\dual[B\cat M]{\Para(\bullet)}} \& X \& {m \bullet X} \& \textcolor{rgb,255:red,214;green,92;blue,92}{m \bullet X} \& \textcolor{rgb,255:red,214;green,92;blue,92}{Y} \\
{B\cat M} \& \textcolor{rgb,255:red,214;green,92;blue,92}{\ast} \& \textcolor{rgb,255:red,214;green,92;blue,92}{\ast} \& \ast \& \ast
\arrow["m", color={rgb,255:red,214;green,92;blue,92}, from=3-2, to=3-3]
\arrow[Rightarrow, no head, from=3-3, to=3-4]
\arrow[Rightarrow, no head, from=3-4, to=3-5]
\arrow["{m_X}", from=2-2, to=2-3]
\arrow[Rightarrow, no head, from=2-3, to=2-4]
\arrow["f"', color={rgb,255:red,214;green,92;blue,92}, from=2-5, to=2-4]
\arrow["{1_V}", Rightarrow, no head, from=1-4, to=1-5]
\arrow["{m_U}", from=1-2, to=1-3]
\arrow["{f^\sharp}", color={rgb,255:red,214;green,92;blue,92}, from=1-3, to=1-4]
\arrow["{\dual[B\cat M]{P_\bullet}}", from=2-1, to=3-1]
\arrow["\view", from=1-1, to=2-1]
\end{tikzcd}
\end{equation}

The idea of seeing optics as fibered by (or indexed by) their residual has appeared before in the literature, namely in <cit.>.

§.§ Hofstra's $\Dial$ monad

Hofstra <cit.> defined a monad on fibrations that builds Dialectica-like categories by simple sum-product completion:

\begin{equation}
\Dial(P) = \Sum(\Prod(P)) = \Sum(\dual{\Sum(\dual P)})
\end{equation}

where $P : \cat E \to \cat C$ is a fibration on $\cat C$ cartesian monoidal.

In $\Dial(P)$, objects are triples $(I, X, U : \cat C, \alpha : \cat P(I \times X \times U))$ and morphisms have four parts:

f_0 : I →J

f : I ×X →Y

f^♯: I ×X ×V →U

i : I, x:X,v:V ⊢    f^: α(i, x, f^♯(i,x,v)) →β(f_0(i), f(i,x), v)

If we ignore the duals for a moment (they can be put back later), we see this is actually given by a sequence of three fibrations over $\cat C$:

\begin{equation}
% file:///home/jsb20179/data/software/quiver/src/index.html?q=WzAsOSxbMCwyLCJcXGNhdCBDX1xccHJval5cXGRvd25hcnJvdyJdLFswLDMsIlxcY2F0IEMiXSxbMSwyLCJcXGNhdCBDIl0sWzEsMSwiXFxjYXQgQ19cXHByb2peXFxkb3duYXJyb3ciXSxbMiwxLCJcXGNhdCBDIl0sWzIsMCwiXFxjYXQgRSJdLFsxLDAsIlxcU3VtKHApIl0sWzAsMCwiXFxTdW0oXFxTdW0ocCkpIl0sWzAsMSwiXFxjYXQgQ19cXHByb2peXFxkb3duYXJyb3cgXFx0aW1lc197XFxjYXQgQ30gXFxjYXQgQ19cXHByb2peXFxkb3duYXJyb3ciXSxbNSw0LCJwIl0sWzYsM10sWzYsNV0sWzMsNCwiXFx0aW1lcyJdLFszLDIsIlxcY29kIiwxXSxbMCwyLCJcXHRpbWVzIl0sWzAsMSwicV8xID0gXFxjb2QiLDJdLFs3LDZdLFs3LDgsInFfMyIsMl0sWzgsMCwicV8yIiwyXSxbOCwzXSxbNiw0LCIiLDEseyJzdHlsZSI6eyJuYW1lIjoiY29ybmVyIn19XSxbNywxOSwiIiwxLHsibGV2ZWwiOjEsInN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs4LDE0LCIiLDEseyJsZXZlbCI6MSwic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV1d
\begin{tikzcd}[ampersand replacement=\&]
{\Sum(\Sum(P))} \& {\Sum(P)} \& {\cat E} \\
{\cat C_\proj^\downarrow \times_{\cat C} \cat C_\proj^\downarrow} \& {\cat C_\proj^\downarrow} \& {\cat C} \\
{\cat C_\proj^\downarrow} \& {\cat C} \\
{\cat C}
\arrow["P", from=1-3, to=2-3]
\arrow[from=1-2, to=2-2]
\arrow[from=1-2, to=1-3]
\arrow["\times", from=2-2, to=2-3]
\arrow["\cod"{description}, from=2-2, to=3-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "\times", from=3-1, to=3-2]
\arrow["{Q_1 = \cod}"', from=3-1, to=4-1]
\arrow[from=1-1, to=1-2]
\arrow["{Q_3}"', from=1-1, to=2-1]
\arrow["{Q_2}"', from=2-1, to=3-1]
\arrow[""{name=1, anchor=center, inner sep=0}, from=2-1, to=2-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=0]
\end{tikzcd}
\end{equation}

One can see $\Dial(P)$ is obtained by dualizing the top two:

\begin{equation}
\Dial(P) = \dual[2]{(\Sum(\Sum(P)) \nlongto{Q_3} \cat C_\proj^\downarrow \times_{\cat C} \cat C_\proj^\downarrow \nlongto{Q_2} \cat C_\proj^\downarrow)} \nlongto{Q_1} \cat C
\end{equation}

This readily carries over to the dependent Dialetica construction

\[ \mathfrak{DDial}(P) := \Sigma(\Pi(P))\]

of a fibration $P : \cat E \to \cat B$.[For a finitely complete category $\cat C$, we recover $D\cat C$ as the fiber over the terminal object of $\mathfrak{DDial}(P)$, where $P : \cat E \to \cat B$ is taken to be $\mathsf{Sum}(!) : \mathsf{Sum}(\cat C) \to \mathsf{Sum}(1) \simeq \Set$, arising canonically from the free sum completion of $\cat C$, see <cit.>] Here, the sum completion $\Sigma(P) = \Fam(P)$ is the family construction of a fibration $P$, and $\Pi(P) := \dual{(\Sigma(\dual{P}))}$ is the product completion of a fibration $P$. Thus, the iterated dual is applied to the following composite of fibrations:

\[\begin{tikzcd}
{\Sigma(\Sigma(P))} & {\Sigma(P)} & {\cat E} \\
{\cat B^\downarrow \times_{\cat B} \cat B^\downarrow} & {\cat B^\downarrow} & {\cat B} \\
{\cat B^\downarrow} & {\cat B} \\
{\cat B}
\arrow["P", from=1-3, to=2-3]
\arrow[from=1-2, to=2-2]
\arrow[from=1-2, to=1-3]
\arrow["\dom", from=2-2, to=2-3]
\arrow["\cod"{description}, from=2-2, to=3-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "\dom", from=3-1, to=3-2]
\arrow["{{\cod}}"', from=3-1, to=4-1]
\arrow[from=1-1, to=1-2]
\arrow[from=1-1, to=2-1]
\arrow[from=2-1, to=3-1]
\arrow[""{name=1, anchor=center, inner sep=0}, from=2-1, to=2-2]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-2, to=2-3]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=1]
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-1, to=0]
\end{tikzcd}\]

The elements of the total category of $\mathfrak{DDial}(P)$ are the dependent generalization of the simple case of $\mathfrak{Dial}(P)$:

f_0 : I →J

i:I ⊢   f : X(i) →Y(f(i))

i:I, x:X(i) ⊢   f^♯: V(f(i), f_0(i,x)) →U(i,x)

i:I, x:X(i), y:Y(f(i), f_0(i,x)) ⊢    f^: α(i,x,f_1(i,x,y)) →β(f(i), f_0(i,x), y)

Putting together our observations about the common pattern for categories of lenses, Dialectica, and optics, we arise at the following result. Its proof can be done by unwinding the definitions we gave, verifying that they indeed satisfy the postulated descriptions:

* $P$-lenses are dialenses of height $1$.

* $P$-Dialectica categories (either simple or dependent) are dialenses of height $2$.

* Optics are dialenses of height $2$, coming from the Para construction over the given base symmetric monoidal category.

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

abstractLenses, optics and dependent lenses (or equivalently morphisms of containers, or equivalently natural transformations of polynomial functors) are all widely used in applied category theory as models of bidirectional processes. From the definition of lenses over a finite product category, optics weaken the required structure to actions of monoidal categories, and dependent lenses make use of the additional property of finite completeness (or, in case of polynomials, even local cartesian closure). This has caused a split in the applied category theory literature between those using optics and those using dependent lenses. The goal of this paper is to unify optics with dependent lenses, by finding a definition of fibre optics admitting both as special cases.
annotationComment: This is an extended abstract of a forthcoming paper
notearXiv:2112.11145 [math]
titleFibre optics
ge/R3EQBWA5/Braithwaite et al. - 2021 - Fibre optics.pdf:application/pdf

Aarhus Universitet

Aarhus, DK

titleDialectica Interpretations – A Categorical Analysis

abstractTambara modules are strong profunctors between monoidal categories. They've been defined by Tambara in the context of representation theory, but quickly found their way in applications when it was understood Tambara modules provide a useful encoding of modular data accessors known as mixed optics. To suit the needs of these applications, Tambara theory has been extended to profunctors between categories receiving an action of a monoidal category. Motivated by the generalization of optics to dependently-typed contexts, we sketch a further extension of the theory of Tambara modules in the setting of actions of double categories (thus doubly indexed categories), by defining them as horizontal natural transformations. The theorems and constructions in Pastro-Street theory relevant to profunctor representation theorem for mixed optics are reobtained in this context. This reproduces the definition of dependent optics recently put forward by Vertechi and Milewski, and hinted at by previous work of the author and his collaborators.
annotationComment: 17 pages, 1 figure
notearXiv:2204.10708 [math]
titleSeeing double through dependent optics
ge/YN8H4QHK/Capucci - 2022 - Seeing double through dependent optics.pdf:application/pdf

abstractOptics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.
annotationComment: 38 pages. Final version with Compositionality metadata, does not change theorem numbering
notearXiv:2001.07488 [cs, math]
titleProfunctor Optics, a Categorical Update
ge/DSBCRTBT/Clarke et al. - 2024 - Profunctor Optics, a Categorical Update.pdf:application/pdf

Open Publishing Association

journaltitleElectronic Proceedings in Theoretical Computer Science
titleTowards Foundations of Categorical Cybernetics

Cambridge University Press

titleAn invitation to applied category theory: seven sketches in compositionality

abstractOptics 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.
annotationComment: 28 pages
notearXiv:2209.09351 [cs, math]
titleSpace-time tradeoffs of lenses and optics via higher category theory
ge/DFZFZPE8/Gavranović - 2022 - Space-time tradeoffs of lenses and optics via high.pdf:application/pdf

abstractWe consider some basic properties of the 2-category Fib of fibrations over arbitrary bases, exploiting the fact that it is fibred over Cat. We show a factorisation property for adjunctions in Fib, which has direct consequences for fibrations, e.g. a characterisation of limits and colimits for them. We also consider oplax colimits in Fib, with the construction of Kleisli objects as a particular example. All our constructions are based on an elementary characterisation of Fib as a 2-fibration.
journaltitleJournal of Pure and Applied Algebra
titleSome properties of Fib as a fibred 2-category
ome properties of Fib as a fibred 2-category.pdf:application/pdf;ScienceDirect Snapshot:/home/jsb20179/Zotero/storage/7J2EC7JC/S0022404997001291.html:text/html

abstractA pattern of interaction that arises again and again in programming is a "handshake", in which two agents exchange data. The exchange is thought of as provision of a service. Each interaction is initiated by a specific agent–the client or Angel–and concluded by the other–the server or Demon. We present a category in which the objects–called interaction structures in the paper–serve as descriptions of services provided across such handshaken interfaces. The morphisms–called (general) simulations–model components that provide one such service, relying on another. The morphisms are relations between the underlying sets of the interaction structures. The proof that a relation is a simulation can serve (in principle) as an executable program, whose specification is that it provides the service described by its domain, given an implementation of the service described by its codomain. This category is then shown to coincide with the subcategory of "generated" basic topologies in Sambin's terminology, where a basic topology is given by a closure operator whose induced sup-lattice structure need not be distributive; and moreover, this operator is inductively generated from a basic cover relation. This coincidence provides topologists with a natural source of examples for non-distributive formal topology. It raises a number of questions of interest both for formal topology and programming. The extra structure needed to make such a basic topology into a real formal topology is then interpreted in the context of interaction structures.
notearXiv:0905.4063 [cs, math]
titleProgramming interfaces and basic topology
ge/QS5LM6Q2/Hancock and Hyvernat - 2009 - Programming interfaces and basic topology.pdf:application/pdf

journaltitleModels, logics, and higherdimensional categories: A tribute to the work of Mihály Makkai
titleThe Dialectica monad and its cousins

journaltitleAnnals of Pure and Applied Logic
noteTroelstra Festschrift
titleProof theory in the abstract

journaltitleTheoretical Computer Science
notePublisher: Elsevier
titleComprehension categories and the semantics of type dependency

titleComment on `The n-Category Café'

Oxford, United Kingdom

Association for Computing Machinery

booktitle33rd Annual ACM/IEEE Symposium on Logic in Computer Science
titleDialectica Models of Type Theory

abstractSimple optics are defined using actions of monoidal categories. Compound optics arise, for instance, as natural transformations between polynomial functors. Since a monoidal category is a special case of a bicategory, we formulate complex optics using the action of a bicategory. We show that polynomial optics are a special case of complex optics defined by the action of bicategory $\mathbf{Prof}$ on co-presheaves.
annotationComment: 9 pages
notearXiv:2203.12022 [math]
titleCompound Optics
ge/GLAFADBA/Milewski - 2022 - Compound Optics.pdf:application/pdf

noteTalk at 2022 Workshop on Polynomial Functors, Topos Institute
titleDependent products of polynomials

University of Cambridge

Cambridge, UK

titleThe Dialectica Models of Type Theory

abstractEvery Grothendieck ﬁbration gives rise to a vertical/cartesian orthogonal factorization system on its domain. We deﬁne a cartesian factorization system to be an orthogonal factorization in which the left class satisﬁes 2-of-3 and is closed under pullback along the right class. We endeavor to show that this deﬁnition abstracts crucial features of the vertical/cartesian factorization system associated to a Grothendieck ﬁbration, and give comparisons between various 2-categories of factorization systems and Grothendieck ﬁbrations to demonstrate this relationship. We then give a construction which corresponds to the ﬁberwise opposite of a Grothendieck ﬁbration on the level of cartesian factorization systems.
annotationComment: 20 pages
notearXiv:2006.14022 [math]
titleCartesian Factorization Systems and Grothendieck Fibrations
18A32,Mathematics - Category Theory

noteUnpublished book draft. Available at <http://davidjaz.com/Papers/DynamicalBook.pdf>
titleCategorical systems theory

titlePolynomial Functors: A Mathematical Theory of Interaction

journaltitleCategories in Computer Science and Logic
notePublisher: Contemp. Math
titleThe Dialectica categories

abstract<p>Data accessors allow one to read and write components of a data structure, such as the fields of a record, the variants of a union, or the elements of a container. These data accessors are collectively known as optics; they are fundamental to programs that manipulate complex data. Individual data accessors for simple data structures are easy to write, for example as pairs of ‘getter’ and ‘setter’ methods. However, it is not obvious how to combine data accessors, in such a way that data accessors for a compound data structure are composed out of smaller data accessors for the parts of that structure. Generally, one has to write a sequence of statements or declarations that navigate step by step through the data structure, accessing one level at a time—which is to say, data accessors are traditionally not first-class citizens, combinable in their own right.</p> <br/> <p>We present a framework for modular data access, in which individual data accessors for simple data structures may be freely combined to obtain more complex data accessors for compound data structures. Data accessors become first-class citizens. The framework is based around the notion of profunctors, a flexible generalization of functions. The language features required are higher-order functions (‘lambdas’ or ‘closures’), parametrized types (‘generics’ or ‘abstract types’) of higher kind, and some mechanism for separating interfaces from implementations (‘abstract classes’ or ‘modules’). We use Haskell as a vehicle in which to present our constructions, but other languages such as Scala that provide the necessary features should work just as well. We provide implementations of all our constructions, in the form of a literate program: the manuscript file for the paper is also the source code for the program, and the extracted code is available separately for evaluation. We also prove the essential properties, demonstrating that our profunctor-based representations are precisely equivalent to the more familiar concrete representations. Our results should pave the way to simpler ways of writing programs that access the components of compound data structures.</p>
journaltitleArt, Science, and Engineering of Programming
notePublisher: Aspect-Oriented Software Association
shorttitleProfunctor optics
titleProfunctor optics: Modular data accessors

titleCategories of optics

Cambridge University Press

booktitleMathematical proceedings of the Cambridge philosophical society
titleLocally cartesian closed categories and type theory

titleGeneralized Lens Categories via functors $\mathcal{C}^{\rm op}\to\mathsf{Cat}$

titleFibered Categories a la Jean Benabou

titleThe Gödel Fibration

abstractA 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 the 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.
annotationComment: In Proceedings ACT 2022, arXiv:2307.15519
journaltitleElectronic Proceedings in Theoretical Computer Science
notearXiv:2204.09547 [cs, math]
titleDependent Optics
ge/X228DJQY/Vertechi - 2023 - Dependent Optics.pdf:application/pdf

University of Cambridge

Cambridge, UK

titlePolynomials and models of type theory