Database Reference
In-Depth Information
Proposition 60
Denotational semantics of each simple mapping f
,
between any
two database instances A and B
,
is given by the unique equivalent “computa-
tion” arrow f
1
f in T
coalg
from the monadic T-coalgebra (A,η
A
) into
the cofree monadic T-coalgebra (T B,μ
B
)
,
f
1
:
η
B
◦
(T B,μ
B
) or
,
dually
,
(A,η
A
)
−→
by the unique equivalent arrow f
OP
1
f)
OP
f
OP
η
OP
B
(η
B
◦
=
◦
from the free
monadic T-algebra (T B,μ
B
) into the monadic T-algebra (A,η
OP
)
.
A
Proof
We have to show that for any morphism
f
:
A
→
B
between an object
A
=
1
≤
j
≤
m
A
j
,m
=
1
≤
i
≤
k
B
i
,k
1,
μ
B
◦
≥
1 and
B
≥
η
B
◦
f
=
T(η
B
◦
f)
◦
η
A
is
valid. In fact, by Proposition
57
,
η
B
is the isomorphism
is
B
:
B
→
TB
, so that
T is
B
=
id
TB
:
TB
→
TB
, due to the fact that
T is
B
i
:
TB
i
→
TB
i
|
T is
B
=
is
B
is
B
i
∈
(
from
T is
B
i
=
id
TB
i
=
TB
i
,Tis
B
i
=
id
TB
i
)
id
TB
i
:
is
B
=
TB
i
→
TB
i
|
is
B
i
∈
={
id
TB
i
|
1
≤
i
≤
k
}
id
TB
=
,
and
μ
B
=
id
TB
. Consequently,
μ
B
◦
η
B
◦
f
=
id
TB
◦
is
B
◦
f
=
is
B
◦
f
, so that
is
B
◦
f
μ
B
◦
η
B
◦
f
=
is
B
i
◦
f
ji
f
f
ji
∈
is
B
i
∩
f
ji
=
TB
i
∩
f
ji
=
f
ji
f.
=
f
f
f
f
ji
∈
f
ji
∈
f
ji
∈
Analogously,
T(η
B
◦
f)
◦
η
A
=
Tη
B
◦
Tf
◦
is
A
=
id
TB
◦
Tf
◦
is
A
=
Tf
◦
is
A
. Thus,
Tf
◦
is
A
T(η
B
◦
f)
◦
η
A
=
Tf
ji
◦
is
A
j
f
f
ji
∈
Tf
ji
∩
is
A
j
=
Tf
ji
∩
=
TA
j
f
f
f
ji
∈
f
ji
∈
Tf
ji
Tf
(by Theorem
2
)
f.
=
f
f
ji
∈
