=Paper=
{{Paper
|id=Vol-1396/p1-johnson
|storemode=property
|title=Spans of Delta Lenses
|pdfUrl=https://ceur-ws.org/Vol-1396/p1-johnson.pdf
|volume=Vol-1396
|dblpUrl=https://dblp.org/rec/conf/staf/JohnsonR15
}}
==Spans of Delta Lenses==
https://ceur-ws.org/Vol-1396/p1-johnson.pdf
Spans of Delta Lenses
Michael Johnson
Departments of Mathematics and Computing, Macquarie University
Robert Rosebrugh
Department of Mathematics and Computer Science
Mount Allison University
Abstract
As part of an ongoing project to unify the treatment of symmetric lenses
(of various kinds) as equivalence classes of spans of asymmetric lenses
(of corresponding kinds) we relate the symmetric delta lenses of Diskin
et al, with spans of asymmetric delta lenses. Because delta lenses are
based on state spaces which are categories rather than sets there is
further structure that needs to be accounted for and one of the main
findings in this paper is that the required equivalence relation among
spans is compatible with, but coarser than, the one expected. The
main result is an isomorphism of categories between a category whose
morphisms are equivalence classes of symmetric delta lenses (here called
fb-lenses) and the category of spans of delta lenses modulo the new
equivalence.
1 Introduction
In their 2011 POPL paper [4] Hoffmann, Pierce and Wagner defined and studied (set-based) symmetric lenses.
Since then, with the study of variants of asymmetric lenses (set-based or otherwise), there has been a need
for more definitions of corresponding symmetric variants. This paper is part of an ongoing project by the
authors to develop a unified theory of symmetric and asymmetric lenses of various kinds. The goal is to make it
straightforward to define the symmetric version of any, possibly new, asymmetric lens variant (and conversely).
Once an asymmetric lens is defined the unified theory should provide the symmetric version (and vice-versa).
In [4] Hoffmann et al noted that there were two approaches that they could take to defining symmetric lenses.
One involved studying various right and left (corresponding to what other authors call forwards and backwards)
operations. The other would be based on spans of asymmetric lenses. In both cases an equivalence relation was
needed to define composition of symmetric lenses, to ensure that that composition is associative, and to identify
lenses which were equivalent in their updating actions although they might differ in “hidden” details such as
their complements (see [4]) or the head (peak) of their spans. Hoffmann et al gave their definition of symmetric
lens in terms of left and right update operations, noting that “in the span presentation there does not seem to
be a natural and easy-to-use candidate for . . . equivalence”.
In [6] the present authors developed the foundations needed to work with spans of lenses of various kinds
and proposed an equivalence for spans of well-behaved set-based asymmetric lenses (called here HPW-lenses)
and also for several other set-based variants. Our goal was to find the finest equivalence among spans of HPW
lenses that would satisfy the requirements of the preceding paragraph. Such an equivalence needed to include,
and be coarser than, span equivalence (an isomorphism between the heads of the spans commuting with the
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: A. Cunha, E. Kindler (eds.): Proceedings of the Fourth International Workshop on Bidirectional Transformations (Bx 2015),
L’Aquila, Italy, July 24, 2015, published at http://ceur-ws.org
1
legs of the spans). Furthermore pre-composing the legs of a span of HPW lenses with a non-trivial HPW lens
gives a new span which differs from the first only in the “hidden” details — the head would be different but the
updating actions at the extremities would be the same — so such pairs of spans should also be equivalent. In [6]
we were able to show that the equivalence generated by such non-trivial HPW lenses (commuting with the legs
of the spans) worked well, and that result was very satisfying because it demonstrated, as so much work in the
theory of lenses does, that lenses and bidirectional transformations more generally are valuable generalisations
of isomorphisms.
Of course, the work so far, being entirely set-based, is still far from a unified theory, so in this paper we turn
to the category-based delta-lenses of Diskin, Xiong and Czarnecki [1] and study the symmetric version derived
from spans of such lenses and compare it with the symmetric (forwards and backwards style) version that Diskin
et al propose in [2].
The paper is structured as follows. In Sections 2 and 3 we review and develop the basic mathematical
properties of delta-lenses (based on [1] and referred to here as d-lenses) and symmetric delta lenses (based on [2],
and called here fb-lenses after their basic operations called “forwards” and “backwards”, thus avoiding clashing
with the general use of “symmetric” for equivalence reduced spans of lenses). As in the work of Hoffmann et al,
both fb-lenses and spans of d-lenses need to be studied modulo an equivalence relation and the two equivalence
relations we propose are introduced in Section 4. In Section 5 we show that using the two equivalences does indeed
yield a category of (equivalence classes of) fb-lenses and a category of (equivalence classes of) spans of d-lenses
respectively (and of course, we need to show that the equivalence relations we have introduced are congruences
in order to construct the categories). Finally in Section 6 we explore the relationship between the two categories
and show that there is an equivalence of categories, indeed in this case an isomorphism of categories, between
them.
Because of the usefulness of category-based lenses (in particular delta-lenses) in applications, the work pre-
sented here lays important mathematical foundations. Furthermore the extra mathematical structure provided
in the category-based variants has revealed a surprise — an equivalence generated by non-trivial lenses is not
coarse enough to ensure that two spans of d-lenses with the same fb-behaviour are always identified. The diffi-
culty that arises is illustrated in a short example and amounts to “twisting” the structures so that no single lens
can commute with the lenses on the left side of the spans, and at the same time commute with the lenses on the
right side of the spans. The solution, presented as one of the equivalences in Section 4, relaxes the requirement
that the comparison be itself a lens, and asks that it properly respect the put operations on both sides (rather
than having its own put operation commuting with both sides).
2 Asymmetric delta lenses
For any category C, we write |C| for the set (discrete category) of objects of C and C2 for the category whose
objects are arrows of C. For a functor G : S / V, denote the “comma” category, whose objects are pairs
consisting of an object S of S and an arrow α : GS / V , by (G, 1V ) . We recall the definition of a delta lens
(or d-lens) [1, 5]:
Definition 1 A (very well-behaved) delta lens (d-lens) from S to V is a pair (G, P ) where G : S / V is a
functor (the “Get”) and P : |(G, 1V )| / |S2 | is a function (the “Put”) and the data satisfy:
(i) d-PutInc: the domain of P (S, α : GS / V ) is S
(ii) d-PutId: P (S, 1GS : GS / GS) = 1S
(iii) d-PutGet: GP (S, α : GS /V)=α
(iv) d-PutPut: P (S, βα : GS /V / V 0 ) = P (S 0 , β : GS 0 / V 0 )P (S, α : GS / V ) where S 0 is the codomain
of P (S, α : GS /V)
For examples of d-lenses, we refer the reader to [1]. Meanwhile, we offer a few sentences here to help orient the
reader to the notations used. Both the categories S and V represent state spaces. Objects of S are states and an
arrow S / S 0 of S represents a specific transition from the state S which is its domain to the state S 0 which is
its codomain. Such specified transitions are often called “deltas”. Similarly for V. A functor G : S / V maps
states of S to states of V — S is sent to GS. Furthermore, being a functor it maps deltas S / S 0 in S to deltas
GS / GS 0 in V. The objects of (G, 1V ) are important because, being a pair (S, α : GS / V ), they encapsulate
2
both an object of S and a delta starting at GS. Such a pair is the basic input for a Put operation. The Put
operation P itself, in the case of a d-lens, is just a function (not a functor) and it takes such an “anchored delta”
(S, α : GS / V ) in V to a delta in S which, by d-PutInc, starts at S. The axioms d-PutId and d-PutPut ensure
that the P operation respects composition, including identities. Finally, the axiom d-PutGet ensures that, as
expected, the Put operation results in a delta in S which is carried by G to α, the given input delta.
In [5], we proved that d-lenses compose, that a c-lens as defined there is a special case of d-lens and that their
composition is as for d-lenses, and finally that d-lenses are strictly more general than c-lenses. We also proved
that d-lenses are certain algebras for a semi-monad.
Furthermore, in [6] we developed the technique to compose spans of lenses in general. For d-lenses, this
specializes to Definition 3. We first need a small but important proposition, and we formally remind the reader
about our notations for spans and cospans.
A span is a pair of morphisms, with common domain:
S?
u ??v
??
X Y
Despite the symmetry, such a span is often described as a “span from X to Y ”, and is distinguished from the
same two arrows viewed as a span from Y to X. The illustrated span above is often denoted for brevity’s sake
u:Xo S / Y : v and, when X, S and Y are understood or easily derived, we sometimes just refer to it as the
span u, v. The object S is sometimes called the head or peak of the span and the arrows u and v are called the
legs of the span. The objects X and Y are, naturally enough, called the feet of the span. Cospans are described
and notated in the same way but the arrows u and v are reversed. Finally, if, as sometimes is necessary, a span
is drawn upside down, the common domain is still called the head despite being drawn below the feet.
When working with spans it is often necessary to calculate pullbacks. For simplicity of presentation we will
usually assume that the pullback has been chosen so that its objects and morphisms are pairs of objects from
the categories from which it has been constructed (so, for example, in the diagram below, objects of T are pairs
of objects (S, W ) from the categories S and W respectively, with the property that G(S) = H(W ), and similarly
for morphisms of T).
Proposition 2 Let G : S /Vo W : H be a cospan of functors. Suppose that P : |(G, 1V )| / |S2 | is a
function which, with G, makes the pair (G, P ) a d-lens. Then, in the pullback square in cat:
T KK 0
H 0 sss KKGK
s
ysss K%
S KK W
KKK
K sss
G K% ysss
H
V
the functor G0 together with P 0 : |(G0 , 1W )| / |T2 | defined by P 0 ((S, W ), β : G0 (S, W ) / W 0 ) = (P (S, H(β)), β) :
(S, W ) / (S 0 , W 0 ) define a d-lens from T to W.
Proof. Note first that P 0 makes sense since H(β) is a morphism HG0 (S, W ) / H(W 0 ) but HG0 (S, W ) =
GH 0 (S, W ) = GS so it is in fact a morphism GS / H(W 0 ). Furthermore we denote the codomain of P (S, H(β))
by S 0 so that G(S 0 ) = H(W 0 ) and thus (S 0 , W 0 ) is an object of T. The d-PutInc, d-PutId and d-PutGet
conditions on (G0 , P 0 ) are satisfied by construction. The d-PutPut condition follows immediately from d-PutPut
for (G, P ).
This means we can talk about the “pullback” of a d-lens along an arbitrary functor, in particular along the
Get of another d-lens. This is similar to the situations described in [6]. The inverted commas around “pullback”
are deliberate because the constructed d-lens may not be an actual pullback in the category of d-lenses (the
category whose objects are categories and whose arrows S / V are d-lenses from S to V).
3
Definition 3 Suppose that in
T KK
H sss KKK
s KK
ysss % 0
S KKK s S KKKKFR
GL sss KKK s
ss
GR K%
ss KKK
yss yss FL %
X Y Z
the functors GL , GR , FL , and FR are the Gets of d-lenses with corresponding Puts PL , PR , QL , and QR , and T
is the pullback of GR and FL . For the “pullback” d-lenses with Gets H and K, denote the Puts by PH and PK .
Then the span composite of the span of d-lenses (GL , PL ), (GR , PR ) from X to Y with the span of d-lenses
(FL , QL ), (FR , QR ) from Y to Z, denoted
((GL , PL ), (GR , PR )) ◦ ((FL , QL ), (FR , QR ))
is the span of d-lenses from X to Z specified as follows. The Gets are GL H and FR K. The Puts are those for
the composite d-lenses (GL , PL )(H, PH ) and (FR , QR )(K, PK ).
In a sense, the composite just defined corresponds to the ordinary composite of spans in a category with
pullbacks. In the category of categories, the ordinary span composition of the span GL , GR and with the span
FL , FR is the span GL H, FR K. As usual for such composites, the operation is not associative without introducing
an equivalence relation and we do so later in this paper.
3 Symmetric delta lenses
A symmetric delta lens (called an “fb-lens” below) is between categories, say X and Y. It consists of a set
of synchronizing “corrs”, so named because the make explicit intended correspondences between objects of X
and objects of Y, together with “propagation” operations. In the forward direction, given objects X and Y
synchronized by a corr r and an arrow x with domain X, the propagation returns an arrow y with domain Y
and a corr synchronizing the codomains of x and y. This is made precise in the following definition and is based
on definitions in [2] and [3]. We denote the domain and codomain of an arrow x by d0 (x), d1 (x).
Definition 4 Let X and Y be categories. An fb-lens from X to Y is M = (δX , δY , f, b) : X ←→ Y specified as
follows. The data δX , δY are a span of sets
δX : |X| o RXY / |Y| : δY
An element r of RXY is called a corr. For r in RXY , if δX (r) = X, δY (r) = Y the corr is denoted r : X ↔ Y .
The data f and b are operations called forward and backward propagation:
f : Arr(X) ×|X| RXY / Arr(Y) ×|Y| RXY
b : Arr(Y) ×|Y| RXY / Arr(X) ×|X| RXY
where the pullbacks (also known as fibered products) mean that if f(x, r) = (y, r0 ), we have d0 (x) = δX (r), d1 (y) =
δY (r0 ) and similarly for b. We also require that d0 (y) = δY (r) and δX (r0 ) = d1 (x), and the similar equations for
b.
Furthermore, we require that both propagations respect both the identities and composition in X and Y, so
that we have:
r : X ↔ Y implies f(idX , r) = (idY , r) and b(idY , r) = (idX , r)
and
f(x, r) = (y, r0 ) and f(x0 , r0 ) = (y 0 , r00 ) imply f(x0 x, r) = (y 0 y, r00 )
and
b(y, r) = (x, r0 ) and b(y 0 , r0 ) = (x0 , r00 ) imply b(y 0 y, r) = (x0 x, r00 )
4
If f(x, r) = (y, r0 ) and b(y 0 , r) = (x0 , r00 ), we display instances of the propagation operations as:
r r
Xo /Y
X o /Y
x f y x0
b y0
/ o
0 _ _/ Y 0
X o _
0
_ X 0 _o _ 00_ _/ Y 0
r r
For examples of fb-lenses we refer the reader to [2].
Definition 5 Let M = (δX , δY , f , b ) and M 0 = (δY
R R R R S S S S
, δZ , f , b ) be two fb-lenses. We define the composite
0
fb-lens M M = (δX , δZ , f, b) as follows. Let TXZ be the pullback of categories in
TXZ K
δ1 ss KKδK2
ysss K%
RXY K SYZ
KKK ss
R
δY
K% ysss S
δY
|Y|
Let δX = δX R
δ1 : TXZ / X and δZ = δ S δ2 . The operations for M 0 M are defined as follows. Denote f R (x, r) =
Z
(y, rf ), f (y, s) = (z, sf ) and bS (z, s0 ) = (y, sb ), bR (y, r0 ) = (x, rb ). Then
S
f(x, (r, s)) = (z, (rf , sf )) and b(z, (r0 , s0 )) = (x, (rb , sb ))
The diagram
r s
Xo /Y o
/Z
R y S
x
f / f / z
X 0 _o _rf_ _/ Y 0 o_ _sf_ _/ Z 0
shows that the arities are correct for f in the forward direction. That is, we have
f : Arr(X) ×|X| TXZ / Arr(Z) ×|Z| TXZ
and similarly
b : Arr(Z) ×|Z| TXZ / Arr(X) ×|X| TXZ
It is easy to show that the f and b just defined respect composition and identities in X and Z and we record:
Proposition 6 The composite M 0 M just defined is an fb-lens from X to Z.
We note that because it is defined using a pullback, this construction of the composite of a pair of fb-lenses is
not associative, and when we later define a category of fb-lenses the arrows will be equivalence classes of fb-lenses.
Next we define two constructions relating spans of d-lenses with fb-lenses.
We first consider a span of d-lenses. Let L = (GL , PL ) where GL : S / V and K = (GK , PK ) where
GK : S / W be (a span of) d-lenses.
Construct the fb-lens ML,K = (δV , δW , f, b) as follows:
– the corrs are RV,W = |S| with δV S = GL S and δW S = GK S;
– forward propagation f for v : V / V 0 and S : V ↔W is defined by f(v, S) = (w, S 0 ) where w = GK (PL (S, v))
and S 0 is the codomain of PL (S, v);
– backward propagation b is defined analogously.
Lemma 7 ML,K is an fb-lens.
5
Proof. Identity and compositionality for ML,K follow from functoriality of the Gets for L and K and the
d-PutId and d-PutPut equations in Definition 1.
In the other direction, suppose that M = (δV , δW , f, b) is an fb-lens from V to W with
δV : |V| o R / |W| : δW
We now construct a span of d-lenses LM : V o S / W : KM from V to W. The first step is to define
the head S of the span. The set of objects of S is the set R of corrs of M . The morphisms of S are defined as
follows: For objects r and r0 , S(r, r0 ) = {(v, w) | d0 v = δV (r), d1 v = δV (r0 ), d0 w = δW (r), d1 v = δW (r0 )} (where
we write, as usual, S(r, r0 ) for the set of arrows of S from r to r0 ). Thus an arrow may be thought of as a formal
square:
r
V o /W
v w
V0 o / W0
r0
Composition is inherited from composition in V and W at boundaries, or more precisely, for (v, w) ∈ S(r, r0 )
and (v 0 , w0 ) ∈ S(r0 , r00 ) we define:
(v 0 , w0 )(v, w) = (v 0 v, w0 w)
in S(r, r00 ). The identities are pairs of identities. It is easy to see that S is a category.
Next we define the d-lens LM to be the pair (GL , PL ) where we define GL : S / V on objects by δV , and
on arrows by projection, that is GL (v, w) = v. The Put for LM , PL : |(GL , 1V )| / |S2 |, is defined on objects
(r, v : GL (r) / V 0 ) of the category (GL , 1V ) by PL (r, v) = (v, π0 f(v, r)) which is indeed an arrow of S from r
to π1 f(v, r). (As is usual practice, we write π0 and π1 for the projection from any pair onto its first and second
factors respectively.) We define KM = (GK , PK ) similarly.
Lemma 8 LM = (GL , PL ) and KM = (GK , PK ) is a span of d-lenses.
Proof. GL and GK are evidently functorial. We need to show that PL and PK satisfy (i)-(iv) of Definition 1.
These follow immediately from the properties of of the fb-lens M .
The two constructions above are related. One composite of the constructions is actually the identity.
Proposition 9 For any fb-lens M , with the notation of the constructions above
M = MLM ,KM
Proof. By inspection, the corrs and δ’s of MLM ,KM are those of M . Further, it is easy to see that, for example,
the forward propagation of MLM ,KM is identical to that of M .
However, the other composite of the constructions above, namely the span of d-lenses LML.K , KML.K is not
equal to the original span L, K (because the arrows of the original S have been replaced by the formal squares
described above). We have yet to consider the appropriate equivalence for spans of d-lenses, and we do so now.
We will see that LML.K , KML.K is indeed equivalent to L, K.
4 Two equivalence relations
Our first equivalence relation is on spans of d-lenses from X to Y.
Suppose that
(GL ,PL ) (GR ,PR ) (G0L ,PL
0
) (G0R ,PR
0
)
Xo S /Y and X o S0 /Y
are such spans.
The functor Φ : S / S0 is said to satisfy conditions (E) if:
0 0
(1) GL Φ = GL and GR Φ = GR
6
(2) Φ is surjective on objects
α α
(3) whenever ΦS = S 0 , we have both PL0 (S 0 , G0L S 0 / X) = ΦPL (S, GL S / X) and
β β
PR0 (S 0 , G0R S 0 / Y ) = ΦPR (S, GR S / Y ).
By (1) any such Φ is a “2-cell” in spans of categories between the two X to Y spans GL , GR and G0L , G0R .
Moreover, Φ is required both to be surjective on objects and also to satisfy (3), a condition which expresses a
compatibility with the Puts. Notice that the identity functor on S satisfies conditions (E).
Definition 10 Let ≡Sp be the equivalence relation on spans of d-lenses from X to Y which is generated by
functors Φ satisfying (E).
To simplify describing ≡Sp we now prove some properties of functors satisfying conditions (E).
Lemma 11 A composite of d-lens span morphisms satisfying (E) also satisfies (E).
Proof. Suppose that we have spans of d-lenses (GL , PL ), (GR , PR ) and (G0L , PL0 ), (G0R , PR0 ) as above, and a third
such span is:
(G00 00
L ,PL ) (G00 00
R ,PR )
Xo S00 /Y
Suppose Φ : S / S0 and Φ0 : S0 / S00 satisfy (E). Properties (1) and (2) for Φ0 Φ are immediate. We show the P 0
L
α
part of property (3) for Φ0 Φ. Suppose Φ0 ΦS = S 00 and consider PL00 (S 00 , G00L S 0 / X). By (E) for Φ and Φ0 , since
α / α α
Φ0 (Φ(S)) = S 00 , we have PL00 (S 00 , G00L S 00 X) = Φ0 PL0 (Φ(S), and G0L Φ(S) / X) = Φ0 ΦPL (S, GL S / X)
as required.
Suppose that Φ satisfies (E). When ΦS = S 0 it follows that GL S = G0L ΦS = G0L S 0 , which we will use below.
Note that if Φ were the Get of a d-lens (although it need not be) then it would be surjective on arrows by the
d-PutGet equation, but not necessarily surjective on hom sets.
Lemma 12 Suppose once again that (GL , PL ), (GR , PR ), (G0L , PL0 ), (G0R , PR0 ) and (G00L , PL00 ), (G00R , PR00 ) are spans
of d-lenses as above. Let Φ : S / S0 o S00 : Φ0 be the functors in a cospan of span morphisms satisfying (E).
Let
T KK 0
Ψ sss KKΨ
s KK
ysss % 00
S KK S
KKK
K s sss
Φ K% yss Φ0
S0
(GT T
L ,PL ) (GT T
R ,PR )
be a pullback in cat. Then there is a span of d-lenses X o T / Y defined by GT = GL Ψ and
L
00
α PL (S,α) PL (S 00 ,α)
PLT ((S, S 00 ), GTL (S, S 00 ) / X) = (S / W, S 00 / W 00 )
and similarly for (GTR , PRT ). Moreover, Ψ and Ψ0 satisfy (E).
Proof. The first point is that (GTL , PLT ) and (GTR , PRT ) actually are d-lenses. We need to know that PLT is
well-defined. Since (S, S 00 ) is an object of the pullback T, we know that Φ(S) = Φ0 (S 00 ) = S 0 , say. We want
α PL (S,α)
PLT ((S, S 00 ), GTL (S, S 00 ) / X) to be an arrow of T, so we need to show that Φ(S / W ) is equal to
00
PL (S 00 ,α)
Φ0 (S 00 / W 00 ). However both are equal to P 0 (S 0 , α) since both Φ and Φ0 satisfy (E). Thus furthermore,
L
00
(W, W ) is an object of T and using this for d-PutPut each of the required d-lens equations is easy to establish.
Next, we show that Ψ and Ψ0 satisfy (E). First of all, the Gets commute by definition. Moreover, both Ψ and
Ψ are surjective on objects because Φ and Φ0 are so.
0
7
It remains to check property (3) for Ψ and Ψ0 . We need to show that whenever Ψ(S, S 00 ) = S, we have
α / U ) = Ψ(PLT ((S, S 00 ), GTL (S, S 00 ) α / U ))
PL (S, GL S
and this follows immediately from the definitions of Ψ and PLT . (Notice that for S = Ψ(S, S 00 ) we have GL S =
α /
G0 ΦS = G0 Φ0 (S 00 ) = G00 (S 00 ) and thus P 00 (S 00 , G00 S 00
L L L L L U ) is well-defined.) Similarly Ψ0 satisfies (3).
Corollary 13 Zig-zags of span morphisms satisfying (E) reduce to spans of span morphisms satisfying (E).
A zig-zag is any string of arrows (ignoring the direction of the indidual arrows so that neighbouring arrows
might be connected head to head or tail to tail as well as tail to head). It follows that any proof that two spans
of d-lenses are ≡Sp equivalent can be reduced to a single span Ψ, Ψ0 of span morphisms satisfying (E).
The second equivalence relation we introduce is on the set of fb-lenses from X to Y. Recall that Diskin et al
[3] defined symmetric delta lenses (our fb-lenses), but they did not consider composing them. Like Hoffman et
al [4] they would find that they need to consider equivalence classes of their symmetric delta lenses in order for
the appropriate composition to be associative. Also like Hoffman et al, there is a need for an equivalence among
their lenses to eliminate artificial differences. In fact, defining an equivalence to restore associativity is easy.
Choosing the correct equivalence to eliminate the artificial differences is more delicate. And what do we mean by
“atificial differences”? Symmetric lenses of various kinds include hidden data — the complements of Hoffmann
et al and the corrs of Diskin et al are examples. The hidden data is important for checking and maintaining
consistency, but different arrangements of hidden data with the same overall effect should not be counted as
different symmetric lenses.
We now introduce such a relation on the set of fb-lenses from X to Y.
Definition 14 Let L = (δX , δY , f, b) and L0 = (δX 0 0
, δY , f 0 , b0 ) be two fb-lenses (from X to Y) with corrs
0 0 0
RXY , RXY . We say L ≡fb L iff there is a relation σ from RXY to RXY with the following properties:
1. σ is compatible with the δ’s, i.e. rσr0 implies δX r = δX
0 0 0 0
r and δY r = δY r
2. σ is total in both directions, i.e. for all r in RXY , there is r0 in RXY
0
with rσr0 and conversely.
3. for all r, r0 , x an arrow of X, if rσr0 and δX r is the domain of x then the first components of f(x, r) and
f 0 (x, r0 ) are equal and the second components are σ related, i.e. π0 f(x, r) = π0 f 0 (x, r0 ) and π1 f(x, r)σπ1 f 0 (x, r0 )
4. the corresponding condition for b, i.e. for all r, r0 , y an arrow of Y, if rσr0 and δX r is the domain of x then
π0 b(y, r) = π0 b0 (y, r0 ) and π1 b(y, r)σπ1 b0 (y, r0 )
Lemma 15 The relation ≡fb is an equivalence relation.
Proof. For reflexivity take σ to be the identity relation; for symmetry take the opposite relation for σ; for
transitivity, the composite relation is easily seen to satisfy conditions 1. to 4.
Lemma 16 For L, L0 as in the definition above, consider a surjection ϕ : RXY / R0
XY compatible with the δ’s
and satisfying the following conditions:
• for corrs r, r0 , and an arrow x of X, if ϕ(r) = r0 and δX r is the domain of x then the first components
of f(x, r) and f 0 (x, r0 ) are equal and the second components are ϕ related, i.e. π0 f(x, r) = π0 f 0 (x, r0 ) and
ϕ(π1 f(x, r)) = π1 f 0 (x, r0 )
• the corresponding condition for b, i.e. for all r, r0 , y an arrow of Y, if ϕ(r) = r0 and δX r is the domain of
x then π0 b(y, r) = π0 b0 (y, r0 ) and ϕ(π1 b(y, r)) = π1 b0 (y, r0 )
The collection of such surjections (viewed as relations) generates the equivalence relation ≡fb .
8
Proof. To see that ≡fb is generated by such surjections, consider the span tabulating the relation σ in ≡fb viz.
0
RXY o σ / RXY .
Notice that each leg is a surjection satisfying the conditions of the lemma. Conversely, any zig-zag of such
surjections defines a relation which is easily seen to satisfy the conditions of Definition 14.
Remark 17 Although ≡fb is generated by zig-zags of certain surjections, we have just seen that any such zig-zag
can be reduced to a single span of such surjections between sets of corrs.
Proposition 18 Suppose that M ≡fb M 0 are fb-lenses from X to Y equivalent by a generator for ≡fb , i.e. a
surjection ϕ : RXY / R0 . Then (LM , KM ) ≡Sp (LM 0 , KM 0 ) as spans of d-lenses from X to Y.
XY
Proof. We first define Φ : S / S0 on objects by ϕ. Notice that Φ is surjective on objects since ϕ is a surjection.
To define Φ on arrows of S, consider an arrow
r
Xo /Y
x y
X0 o / Y0
r0
of S. Its image under Φ is defined to be the arrow
ϕ(r)
Xo /Y
x y
X0 o / Y0
ϕ(r 0 )
which is an arrow of S0 since ϕ is compatible with the δs. This Φ is evidently functorial and commutes with the
x / 0
Gets. It remains to show that Φ satisfies condition (3) of (E), that is, whenever Φ(r) = r0 , PL0 (r0 , G0L r0 X)=
x / 0 0
ΦPL (r, GL r X ) (with the similar equation holding for PK ).
Now, when r0 = Φ(r), we have
PL0 (r0 , x) = (x, π0 f 0 (x, r0 ))
= (x, π0 f(x, r)) see Lemma 16
= Φ(x, π0 f(x, r)) definition of Φ
= ΦPL (r, x)
0
as required. Similarly for PK .
Proposition 19 Suppose that (L, K) ≡Sp (L0 , K 0 ) as spans of d-lenses from X to Y are made equivalent by a
generator for ≡Sp , i.e. a functor Φ : S / S0 satisfying conditions (E). Then ML,K ≡fb ML0 ,K 0 as fb-lenses from
X to Y.
Proof. Let ϕ be the object function of Φ. Since Φ commutes with the Gets, ϕ is compatible with the δ’s.
We need to show that ϕ satisfies the conditions in Lemma 16. Suppose Φ(S) = S 0 and GL (S) is the domain
of x. Then
π0 f(x, S) = GK PL (x, S)
= G0K ΦPL (x, S)
= G0K PL0 (x, S 0 )
= π0 f 0 (x, S 0 )
9
and
ϕπ1 f(x, S) = ϕd1 PL (x, S)
= d1 ΦPL (x, S)
= d1 PL0 (x, S 0 )
= π1 f 0 (x, S 0 )
as required. Similarly for the equations involving b.
5 Two categories of lenses
The collections of lenses so far discussed do not form categories since their composition is not associative. We
are going to use the equivalence relations of the previous section to resolve this, but first we show that the
equivalence relations respect the composites defined above, that is they are “congruences”.
0 0
Proposition 20 Suppose that M = (δX , δY , f R , bR ), M 0 = (δX
0 0
, δY , f R , bR ) and N = (δY
S
, δZ , f S , bS ) are fb-
0
lenses (see the diagram below in which RXY , RXY and SYZ are the corresponding corrs). Further, suppose
/ R0 0 0
ϕ : RXY XY is a generator of ≡fb . Thus M ≡fb M . Then N M ≡fb N M .
Proof. The composite N M has as corrs the pullback TXZ as in Definition 5, and similarly N M 0 has corrs TXZ
0
.
δ1
RXY? o TXZ?
?? ??
δX ? δY ??δ2
?? ??
??
δYS
?
δZ
|X| ϕ |Y| o SYZ / |Z|
?_ ?
?? ? ?
?? 0
0
δX 0
? δY δ2
R0 o
XY XZT0
δ10
In order to show that N M ≡fb N M 0 , we construct ϕ0 : TXZ / T 0 . This is straightforward using the
XZ
0 0 S
universal property of the pullback TXZ , since δY ϕδ1 = δY δ2 .
To finish, we need to check that ϕ0 satisfies the four requirements of Definition 14.
Compatibility with δs is easy when we note that ϕδ1 = δ10 ϕ0 and δ20 ϕ0 = δ2 .
The function ϕ0 is a total relation in both directions since it is surjective. To see that ϕ0 is surjective, note
0
that any element of TXZ can be thought of as a pair (r0 , s) compatible over Y, and since ϕ is surjective, there
exists an r in RXY , necessarily compatible with s, such that ϕ0 (r, s) = (ϕ(r), s) = (r0 , s).
Let f be the forward propagation of the composite N M , as defined in Definition 5, and let f 0 be the forward
propagation of the composite N M 0 . Suppose r0 = ϕ(r) and thus (r0 , s) = ϕ0 (r, s). We need to show that the
first components of f(x, (r, s)) and f 0 (x, (r0 , s)) are equal and that ϕ0 takes the second component of f(x, (r, s))
to the second component of f 0 (x, (r0 , s)).
The first component of f(x, (r, s)) is π0 f S (π0 f R (x, r), s), while the first component of f 0 (x, (r0 , s)) is
0 0
π0 f S (π0 f R (x, r0 ), s), and these are equal since ϕ is a generator of ≡fb implies π0 f R (x, r) = π0 f R (x, ϕ(r)).
The second component of f(x, (r, s)) is (π1 f R (x, r), π1 f S (π0 f R (x, r), s)), while the second component of
0 0
f (x, (r0 , s)) is (π1 f R (x, r0 ), π1 f S (π0 f R (x, r0 ), s)), and ϕ0 of the first equals the second since, as before,
0
0
π0 f R (x, r) = π0 f R (x, ϕ(r)).
The same arguments work for b and b0 .
0 0
Proposition 21 Suppose that M = (δX , δY , f , b ), N = (δY , δZ , f S , bS ) and N 0 = (δY
R R R 0 0
, δZ , f S , bS ) are fb-
0
lenses (see the diagram below in which RXY , SYZ and SYZ are the corresponding corrs). Further, suppose
ϕ : SYZ / S 0 is a generator of ≡fb . Thus N ≡fb N 0 . Then N M ≡fb N 0 M .
YZ
10
Proof. The composite N M has as corrs the pullback TXZ as in Definition 5, and similarly N 0 M has corrs TXZ
0
.
δ2
TXZ / SYZ
δY ??? δ
δ1 ?? Z
??
?
δX δY
R
|X| o RXY_? / |Y| ϕ |Z|
?? _?
? ?
?? ? ??
?
δ10 ?? δY 0 ?? δ0
Z
0 / S0
TXZ 0 YZ
δ2
The proof follows the same argument as in the previous proposition.
Theorem 22 Equivalence classes for ≡fb are the arrows of a category, denoted fbDLens.
Proof. We first note that Propositions 20 and 21 ensure that composition is well-defined independently of
choice of representative. There is an identity fb-lens with obvious structure which acts as an identity for the
composition. It remains only to note that associativity follows by standard re-bracketing of iterated pullbacks.
The re-bracketing function is the ϕ for an ≡fb equivalence.
Proposition 23 Suppose that (GL , PL ), (GR , PR ), (G0L , PL0 ), (G0R , PR0 ), (FL , QL ), and (FR , QR ) are d-lenses
whose Gets are shown in the diagram below. Further, suppose Φ : S / S0 is a functor satisfying properties (E).
Thus the span (GL , PL ), (GR , PR ) is ≡Sp to the span (G0L , PL0 ), (G0R , PR0 ). Then the two possible span composites
are equivalent, that is
((GL , PL ), (GR , PR )) ◦ ((FL , QL ), (FR , QR )) ≡Sp ((G0L , PL0 ), (G0R , PR0 )) ◦ ((FL , QL ), (FR , QR )).
Proof. The top composite span of d-lenses in the diagram below has head T, the pullback of GR and FL (see
Definition 3), similarly T0 is the head of the bottom span composite.
H
S ?o T?
?? ??
GL ? GR ??K
?? ??
? ? ?
FL FR
X ?_ Y o /Z
??
Φ
? ?R
??
G0L ??
? 0 0
GR K
S0 o 0
T0
H
In order to show the claimed equivalence, we construct a functor Φ0 : T / T0 . Since G0 ΦH = FL K, Φ0 is
R
0
defined by applying the universal property of the pullback T .
Since T and T0 are pullbacks of functors, their objects can be taken to be pairs of objects from S and
R, respectively S0 and R. Similarly, their arrows can be taken to be pairs. Also H and K, respectively H 0
and K 0 can be taken to be projections. We can now explicitly describe the action of Φ0 on an arrow of T as
Φ0 (t0 , t1 ) = (Φt0 , t1 ).
As in Definition 3, we denote the Puts of the lenses whose Gets are H and K by PH and PK . Similarly for
H 0 and K 0 . Denote the composite lens (GL , PL )(H, PH ) by (G, P ) and similarly (G0 , P 0 ) = (G0L , PL0 )(H 0 , PH 0 ).
We need to show that Φ0 satisfies the conditions (E). By its construction Φ0 commutes with the Gets, and is
surjective on objects.
It remains to show that whenever Φ(S, R) = (S 0 , R0 ) (which implies that R = R0 and Φ(S) = S 0 ) we have
α α
P 0 ((S 0 , R0 ), G0L H 0 (S 0 , R0 ) / X 0 ) = Φ0 P ((S, R), GL H(S, R) / X 0)
11
and
γ γ
Q0 ((S 0 , R0 ), FR K 0 (S 0 , R0 ) / Z 0 ) = Φ0 Q((S, R), FR K(S, R) / Z 0)
We begin by proving the first equation immediately above. We know that whenever Φ(S) = S 0 ,
α / α /
P 0 (S 0 , G0 L(S 0 )
L X 0 ) = ΦPL (S, GL (S) X 0 ). We calculate
α α
P 0 ((S 0 , R0 ), G0L H 0 (S 0 , R0 ) / X 0) = P 0 ((S 0 , R0 ), G0L (S 0 ) / X 0)
α
= PH 0 ((S 0 , R0 ), PL0 (S 0 , G0L (S 0 ) / X 0 ))
α α
= (PL0 (S 0 , G0L (S 0 ) / X 0 ), QL (R0 , G0R PL0 (S 0 , G0L (S 0 ) / X 0 )))
α / X 0 ), QL (R, G0R ΦPL (S, GL (S) α / X 0 )))
= (ΦPL (S, GL (S)
α α
= Φ0 (PL (S, GL (S) / X 0 ), QL (R, GR PL (S, GL (S) / X 0 )))
α
= Φ0 (PH ((S, R), PL (S, GL (S) / X 0 )))
α
= Φ0 P ((S, R), GL H(S, R) / X 0)
The first step is merely that H 0 is a projection; the second is the definition of P 0 as the Put of the composite
lens whose Get is G0L H 0 ; the third is the definition of PH 0 (see Proposition 2); the fourth uses R0 = R and
the hypothesis stated just before the equations; the fifth follows since Φ commutes with GR and G0R and the
definition of Φ0 ; the sixth is the definition of PH (see Proposition 2); the last is the definition of P as the Put of
the composite lens whose Get is GL H.
To establish the second equation, suppose Φ0 (S, R) = (S 0 , R0 ), whence R = R0 and Φ(S) = S 0 , and so because
Φ satisfies conditions (E), we have
β β
PR0 (S 0 , G0R (S 0 ) / Y 0 ) = ΦPR (S, GR (S) / Y 0)
β
and since GR (S) = G0R Φ(S) = G0R (S 0 ), the right hand side can be written as ΦPR (S, G0R (S 0 ) / Y 0 ). We
calculate
γ γ
Q0 ((S 0 , R0 ), FR K 0 (S 0 , R0 ) / Z 0) = PK 0 ((S 0 , R0 ), QR (R0 , FR (R0 ) / Z 0 ))
γ γ
= (PR0 (S 0 , FL QR (R0 , FR (R0 ) / Z 0 )), QR (R0 , FR (R0 ) / Z 0 ))
β
Before continuing the calculation, we simplify by defining β by (G0R (S 0 ) / Y 0 ) = FL QR (R0 , FR (R0 ) γ / Z 0 ) =
γ
FL QR (R, FR (R) / Z 0 ) after noting that G0 (S 0 ) is the domain of FL QR (R0 , FR (R0 )γZ 0 ) since the T 0 pullback
R
square commutes. Now, continuing the calculation above:
β γ
= (PR0 (S 0 , G0R (S 0 ) / Y 0 , QR (R0 , FR (R0 ) / Z 0 )))
β γ
= (ΦPR (S, GR (S) / Y 0 , QR (R0 , FR (R0 ) / Z 0 )))
β γ
= (ΦPR (S, G0R (S 0 ) / Y 0 , QR (R, FR (R) / Z 0 )))
γ γ
= Φ0 (PR (S, FL QR (R, FR (R) / Z 0 ), QR (R, FR (R) / Z 0 )))
γ γ
= Φ0 PK ((S, R), QR (R, FR (R) / Z 0 ), QR (R, FR (R) / Z 0 ))
γ
= Φ0 Q((S, R), FR K(S, R) / Z 0)
The first step uses that K 0 is a projection and the definition of Q0 as the Put of the composite lens whose Get is
FR0 K 0 ; the second is the definition of PK 0 (see Proposition 2); the third is the definition of β above; the fourth
uses the hypothesis stated before the equations; the fifth uses R = R0 and the note just before the equations;
the sixth uses the definitions of Φ0 and β; the seventh is the definition of PK (see Proposition 2); the last is the
definition of Q as the Put of the composite lens whose Get is FR K.
Like Propositions 20 and 21, there is a reflected version of Proposition 23, showing that equivalent spans of
d-lenses when composed on the left with another span of d-lenses are equivalent.
12
Proposition 24 In notation analogous to Proposition 23,
((GL , PL ), (GR , PR )) ◦ ((FL , QL ), (FR , QR )) ≡Sp ((GL , PL ), (GR , PR )) ◦ ((FL0 , Q0L ), (FR0 , Q0R )).
Theorem 25 Equivalence classes for ≡Sp are the arrows of a category, denoted SpDLens.
Proof. We first note that Proposition 23 and Proposition 24 ensure that composition is well-defined inde-
pendently of choice of representative. There is a span of identity d-lenses which acts as the identity for the
composition. Again, associativity follows by standard re-bracketing of iterated pullbacks of categories. The
re-bracketing functor is the Φ for an ≡Sp equivalence.
6 An isomorphism of categories of lenses
Now that we have the categories fbDLens and SpDLens, we can extend the constructions of Section 3 to functors
on them.
Definition 26 For the ≡fb equivalence class [M ] of an fb-lens M , let A([M ]) be the ≡Sp equivalence class of,
in the notation of Lemma 8, the span LM , KM .
Proposition 27 A is the arrow function of a functor, also denoted A, from fbDLens to SpDLens.
Proof. We need to show that A preserves identities and composition.
For the former denote by MX the identity fb-lens on a category X. We begin by noticing that the category
Xp at the head of the span of d-lenses constructed from MX has as its objects exactly those of X. Its arrows
from X to X 0 are arbitrary pairs of X arrows, both of which are from X to X 0 . Define the functor Φ from the
head X of the identity span on X to Xp by sending an arrow x of X to the pair of arrows (x, x). This functor
Φ satisfies conditions (E), and so A([MX ]) = [X] as required.
Let M and M 0 be a composable pair of fb-lenses from X to Y and Y to Z respectively. The composite fb-lens
M M has as corrs compatible pairs of corrs, one from M and one from M 0 (see Definition 5). The head S of
0
the span of d-lenses constructed from M 0 M has objects compatible pairs of corrs and as arrows from compatible
corrs (r1 , r2 ) to compatible corrs (r10 , r20 ), pairs of arrows, one from X and one from Z as shown
r1 r2
Xo /Y o /Z
x z
X0 o / Y0 o / Z0
r10 r20
On the other hand, the span composite of the spans constructed from M and M 0 has as head a category T whose
objects are pairs of compatible corrs from M and M 0 respectively. The arrows of T are triples of arrows (x, y, z)
as shown
r1
Xo / Y o r2 / Z
x y z
X0 o / Y0 o / Z0
r10 r20
Define the functor Φ from T to S by sending the triple of arrows (x, y, z) to the pair of arrows (x, z). This
functor Φ satisfies conditions (E), and so A([M 0 M ]) = A([M 0 ])A([M ]) as required.
Definition 28 For the ≡Sp equivalence class [L, K] of a span of d-lenses L, K, let S([L, K]) be the ≡fb equiva-
lence class of, in the notation of Lemma 7, the fb-lens ML,K .
Proposition 29 S is the arrow function of a functor, also denoted S, from SpDLens to fbDLens.
13
Proof. We need to show that S preserves identities and composition.
Unlike the previous proof, the preservation of identities and composition is “on the nose”. That is, the
construction applied to the identity gives precisely the identity fb-lens. Moreover, with judicious choice of
pullbacks, the construction applied to the composite of two composable spans of d-lenses is the composite of the
fb-lenses constructed from each of the spans.
Thus S preserves the equivalence class of the identity span and S([L1 , K1 ][L2 , K2 ]) = S([L1 , K1 ])S([L2 , K2 ]).
Theorem 30 The functors A and S are an isomorphism of categories SpDLens ∼
= fbDLens.
Proof. We need to show that the composites AS and SA are identities. Recall first that both A and S have
identity functions as object functions. Considering the arrows, Proposition 9 shows that SA is the identity
functor. We now consider AS.
For a span L, K of d-lenses between X and Y, using the notation of Lemmas 7 and 8, AS([L, K]) =
[LML,K , KML,K ], so we consider the span LML,K , KML,K of d-lenses whose Gets and Puts we denote by FL , QL
and FK , QK respectively. The head of the span is a category we denote SL,K whose objects are the same as
the objects of S, the head of the span L, K. We define an identity on objects functor Φ : S / SL,K on arrows
by Φ(s) = (GL (s), GK (s)) (recalling that arrows of SL,K are pairs of arrows from X and Y, respectively). We
finish by showing that Φ satisfies conditions (E), and so witnesses AS([L, K]) = [L, K].
It remains to show that Φ satisfies conditions (E). Being identity on objects, Φ is certainly surjective on
objects, and it commutes with the Gets by its construction. For condition (3), given an object S 0 of SL,K ,
an object S of S such that ΦS = S 0 , and an arrow α : GL (S) = FL (S 0 ) / X 0 in X, we have PL (S, α) an
arrow of S. We need to show that ΦPL (S, α) = QL (S , α). Since ΦS = S we have S = S 0 . Now QL (S 0 , α) =
0 0
QL (S, α) = (α, π0 f(α, S)), for the forward propagation f of ML,K constructed as in Lemma 7. By that construc-
tion π0 f(α, S) = GK (PL (S, α)). But ΦPL (S, α) = (GL (PL (S, α)), GK (PL (S, α))) = (α, π0 f(α, S)) = QL (S 0 , α).
Thus, since AS([L, K]) = [L, K], AS is the identity.
7 Conclusions
Because asymmetric delta lenses and symmetric delta lenses are so useful in applications, it is important that
we understand them well and provide a firm mathematical foundation. This paper provides such a foundation
by formalizing fb-lenses and their composition, including determining the equivalence required on fb-lenses for
the composition to be well-defined and associative. Furthermore the resultant category fbDLens of fb-lenses is
equivalent, indeed isomorphic, to the category SpDLens of equivalence classes of spans of d-lenses.
This last result, the isomorphism between fbDLens and SpDLens, furthers the program to unify the treatment
of symmetric lenses of type X as equivalence classes of spans of asymmetric lenses of type X, carrying that
program for the first time into category-based lenses. (And that extension came with a surprise — see below.)
Naturally a unified treatment needs to be tested extensively on a wide range of lens types, and more work
remains. The present paper is an important step in the program, and provides a reason to be hopeful that the
unification is close at hand. Indeed, with this work the program encounters the important category-based lenses
for the first time and that substantially widens the base of unified examples.
We end with a distilled example. It shows in a simplified way why the equivalence used here, based on
conditions (E), needs to be coarser than an equivalence generated by lenses commuting with the spans though
it remains compatible with the earlier work. Thus it is also a coarser equivalence relation than might have been
expected based on [6].
The figure below presents two spans of d-lenses. The categories at the head and feet of the spans have been
shown explicitly. In three cases the category has a single non-identify morphism called variously γ, δ and while
in the fourth case the category has two distinct nonidentity morphisms denoted α and β. In all cases objects
and identity morphisms have not been shown. In three cases there are just two objects, while in the fourth case
there are three, with a single object serving as the domain of both α and β.
14
α 44 β
4
ll RRR
v
l llll RRR
R( δ
γ
↓ hRRR Φ ll6 ↓
RRR
RRR lllll
R lll
↓
The arrows displayed in both spans represent (the Gets of) d-lenses. In the lower span the d-lenses are simply
identity d-lenses (the Gets are isomorphisms sending to γ in the left hand leg, and to δ in the right hand leg).
Both of the Puts are then determined. The upper span is made up of two non-identity d-lenses. In both cases
the Gets send both α and β to the one non-identity morphism (γ in the left hand leg and δ in the right hand
leg). We specify the Puts for the upper span (eliding reference to objects in the Puts’ parameters since they can
be easily deduced): PL (γ) = α and PR (δ) = β for the left and right Puts respectively.
Notice that Φ, the functor that sends both α and β to , satisfies conditions (E) showing, as expected, that
the two spans are equivalent. After all, if one traces through the forward and backward behaviours across the
two spans the results at the extremities are in all cases the same, though the intermediate results at the heads of
the spans differ. However, Φ cannot be the Get of a lens which commutes with the other four d-lenses. Indeed,
to commute with the left hand lenses would require PΦ () = α while to commute with the right hand lenses
would require PΦ () = β, but α 6= β.
8 Acknowledgements
This paper has benefited from valuable suggestions by anonymous referees. The authors are grateful for the
careful and insightful refereeing. In addition, the authors acknowledge with gratitude the support of NSERC
Canada and the Australian Research Council.
References
[1] Zinovy Diskin, Yingfei Xiong, Krzysztof Czarnecki (2011), From State- to Delta-Based Bidirec-
tional Model Transformations: the Asymmetric Case, Journal of Object Technology 10, 6:1–25,
doi:10.5381/jot.2011.10.1.a6
[2] Zinovy Diskin, Yingfei Xiong, Krzysztof Czarnecki, Hartmut Ehrig, Frank Hermann and Francesco Orejas
(2011), From State- to Delta-Based Bidirectional Model Transformations: the Symmetric Case, ACM/IEEE
14th International Conference on Model Driven Engineering Languages and Systems: Springer.
[3] Diskin, Z., and T. Maibaum, Category Theory and Model-Driven Engineering: From Formal Semantics
to Design Patterns and Beyond, 7th ACCAT Workshop on Applied and Computational Category Theory,
2012.
[4] Hofmann, M., Pierce, B., and Wagner, D. (2011) Symmetric Lenses. In ACM SIGPLAN-SIGACT Sympo-
sium on Principles of Programming Languages (POPL), Austin, Texas.
[5] Johnson, M. and Rosebrugh, R. (2013) Delta Lenses and Fibrations. Electronic Communications of the
EASST, vol 57, 18pp.
[6] Johnson, M. and Rosebrugh, R. (2014) Spans of Lenses. CEUR Proceedings, vol 1133, 112–118.
15