Lifting twisted coreflections against delta lenses
Bryce Clarke
Inria Saclay
Abstract:
Delta lenses are functors equipped with a functorial choice of
lifts, and generalise the notion of a split opfibration. It is
known that every functor factors (via a comma category) into a
split coreflection followed by a split opfibration, and that
split coreflections lift against split opfibrations --- this is
the main example of a lifting awfs recently introduced by Bourke
[1]. In this talk, I will introduce the notion of *twisted
coreflection* as a split coreflection equipped with certain
additional structure. We will then see that every functor factors
into a twisted coreflection followed by a delta lens, and that
twisted coreflections lift against delta lenses. The main
theorem is that the double categories of twisted coreflections
and delta lenses form a lifting awfs in the sense of Bourke. This
result revolves the question of characterising the L-coalgebras
for the algebraic weak factorisation system for delta lenses [2],
and establishes a deeper understanding on the differences between
delta lenses and split opfibrations. Future work will be
discussed if time allows.
[1] John Bourke, "An orthogonal approach to algebraic weak factorisation
systems", Journal of Pure and Applied Algebra, Vol 227 (2023). [doi:10.1016/j.jpaa.2022.107294,
arXiv:2204.09584]
[2] Bryce Clarke, "The Algebraic Weak Factorisation System for Delta
Lenses", preprint (2023). [arXiv:2305.02732]