Lifting twisted coreflections against delta lenses (Q6589557)

Delta lenses were introduced in 2011 in [\url{https://link.springer.com/chapter/10.1007/978-3-642-24485-8_22}] as a framework for bidirectional transformations [\textit{F. Abou-Saleh} et al., Lect. Notes Comput. Sci. 9715, 1--28 (2018; Zbl 1476.68034)]. Johnson and Rosenbrugh [\url{https://eceasst.org/index.php/eceasst/article/view/2090}] initiated the study of delta lenses using category theory.\N\NThis paper considers a way of comparing delta lenses and split opfibrations: the class of functors that they lift against. These are the twisted coreflections and split coreflections, respectively.\N\NThe synopsis of the paper goes as follows.\N\N\begin{itemize}\N\item[\S 1] recalls the concepts required to state the definition of an algebraic weak factorization system (AWFS).\N\N\item[\S 2] recalls the notion of delta lense [\url{https://link.springer.com/chapter/10.1007/978-3-642-24485-8_22}; \textit{P. J. Freyd} and \textit{G. M. Kelly}, J. Pure Appl. Algebra 2, 169--191 (1972; Zbl 0257.18005)], constructing a thin double category \(\mathbb{L}\mathrm{ens}\)\ of categories, functors and delta lenses [\url{https://bryceclarke.github.io/other/the-double-category-of-lenses.pdf}]. It is shown (Theorem 2.6) that the double category of delta lenses is isomorphic to the double category \(\mathbb{R}\mathrm{LP}\left( \mathbb{J}\right) \)\ of right lifts for a small double category \(\mathbb{J}\). It is also shown that \ has tabulators, which is exploited to show that a delta lens is equivalent to a commutative diagram of functors\N\[\N\begin{array} [c]{ccc} X & \overset{\varphi}{\longrightarrow} & A\\\N& \underset{f\varphi}{\searrow} & \downarrow_{f}\\\N& & B \end{array}\N\]\Nwhere \(\varphi\)\ is bijective-on-objects and \(f\varphi\)\ is a discrete opfibration.\N\N\item[\S 3] introduces a special kind of split coreflection, called a twisted coreflection, constructing the double category \(\mathbb{T}\mathrm{wCoref}\)\ of categories, functors and twisted coreflections. It is shown (Theorem 3.19) that a split coreflection is a twisted coreflection iff it satisfies a certain pushout condition. It is also shown that a twisted coreflection is equivalent to a pushout square in \(\mathcal{C}\mathrm{at}\)\N\[\N\begin{array} [c]{ccc} A_{0} & \overset{\iota_{A}}{\longrightarrow} & A\\\Nf^{\prime}\downarrow & & \downarrow f\\\NX & \underset{\pi}{\longrightarrow} & B \end{array}\N\]\Nwhere \(A_{0}\)\ is a discrete category , \(\iota_{A}\)\ is identity-on-objects, and \(f^{\prime}\)\ is an initial functor.\N\N\item[\S 4] establishes that twisted coreflections and delta lenses form an algebraic weak factorization system on \(\mathcal{C}\mathrm{at}\). The proof is divided into three steps.\N\N\begin{itemize}\N\item[(1)] The author describes a lifting operation on the following cospan of double functors\N\[\N\mathbb{T}\mathrm{wCoref}\overset{U}{\mathrm{\longrightarrow}}\mathbb{S} \mathrm{q}\left( \mathcal{C}\mathrm{at}\right) \overset{V}{\longleftarrow }\mathbb{L}\mathrm{ens}\N\]\N\N\item[(2)] It is shown that each functor admits a factorization as a cofree twisted coreflection followed by a free delta lens.\N\N\item[(3)] It is shown that the induced double functors\N\begin{align*}\N\mathbb{T}\mathrm{wCoref} & \longrightarrow\mathbb{L}\mathrm{LP}\left( \mathbb{L}\mathrm{ens}\right) \\\N\mathbb{L}\mathrm{ens} & \longrightarrow\mathbb{R}\mathrm{LP}\left( \mathbb{T}\mathrm{wCoref}\right)\N\end{align*}\Nare invertible.\N\end{itemize}\N\N\item[\S 5] outlines directions for future work.\N\end{itemize}