Abstract
Delta lenses are functors equipped with a suitable choice of lifts, and are used to model bidirectional transformations between systems. In this paper, we construct an algebraic weak factorisation system whose R-algebras are delta lenses. Our approach extends a semi-monad for delta lenses previously introduced by Johnson and Rosebrugh, and generalises to any suitable category equipped with an orthogonal factorisation system and an idempotent comonad. We demonstrate how the framework of an algebraic weak factorisation system provides a natural setting for understanding the lifting operation of a delta lens, and also present an explicit description of the free delta lens on a functor.
| Original language | English |
|---|---|
| Pages (from-to) | 54-69 |
| Number of pages | 16 |
| Journal | Electronic Proceedings in Theoretical Computer Science, EPTCS |
| Volume | 397 |
| DOIs | |
| Publication status | Published - 14 Dec 2023 |
| Externally published | Yes |
| Event | 6th International Conference on Applied Category Theory, ACT 2023 - Hybrid, College Park, United States Duration: 31 Jul 2023 → 4 Aug 2023 |