Database Reference
In-Depth Information
μ
B
◦
η
A
, so that
μ
B
◦
Thus,
η
B
◦
f
T(η
B
◦
f)
◦
η
B
◦
f
=
T(η
B
◦
f)
◦
η
A
:
A
→
T
2
B
.
Note that each view-map (i.e., a query)
q
A
:
A
−→
TA
is equal to its denotational
(T A,μ
A
)
.
It is well known (see an analog case for Eilenberg-More category in Sect.
8.3
)
that for a Kleisli category there exists an adjunction
(F
T
,G
T
,η
T
,ε
T
)
such that
we obtain the same monad
(T,η,μ)
such that
T
semantics arrow in
T
coalg
,
q
A
:
(A,η
A
)
−→
=
G
T
F
T
,μ
=
G
T
ε
T
F
T
,η
=
η
T
DB
T
(A,B)
,
G
T
(A)
TA,G
T
(h)
Tθ
−
1
(h)
, and for any
(for any arrow
h
∈
=
=
μ
B
◦
DB
(A,B)
,
F
T
(A)
A,F
T
(f )
arrow
f
f
). Let us see now how the Kleisli
category
DB
T
is “internalized” into the
DB
category.
∈
=
=
η
B
◦
Theorem 17
The Kleisli category
DB
T
of the monad (T,η,μ)is isomorphic to the
DB
category
.
That is
,
it may be “internalized” in
DB
by the faithful forgetful functor
K
φθ
−
1
where
,
for any two objects A and B
,
we have the following bijections of the hom-
sets
:
•
(K
0
,K
1
)
DB
such that K
0
is an identity function and K
1
=
:
DB
T
−→
DB
(A,T B)
=
θ
:
DB
T
(A,B) is a Kleisli bijection and
DB
(A,T B)
=
η
OP
•
φ
:
DB
(A,B) such that φ(_)
=
cod(_)
◦
(_) is a
DB
category
bijection
,
respectively
.
We can generalize a “representation” for the
DB
category
(
instead of
Set
category
):
A “representation” of functor K is a pair (Υ,ϕ)
,
where Υ is the total ob-
ject and ϕ
:
DB
T
(Υ, _)
K is a natural isomorphism
.
The functor
DB
T
(Υ, _)
:
DB
defines the “internalized” hom-sets in
DB
T
,
i
.
e
.,
DB
T
(Υ,B)
TB
Υ
DB
T
−→
and
DB
T
(Υ,f
T
)
Tθ
−
1
(f
T
)
.
id
Υ
⊗
Proof
Let us show that
φ
is really a bijection in
DB
. For any program morphism
f
η
O
B
◦
:
A
−→
TB
we obtain
φ(f)
=
f
:
A
−→
B
and, vice versa, for any
g
:
B
its inverse
φ
−
1
(g)
g
, thus,
φφ
−
1
(g)
η
O
B
◦
A
−→
η
B
◦
=
φ(η
B
◦
g)
=
(η
B
◦
g
(because
η
B
is an isomorphism) and hence
φφ
−
1
is an identity function. Analogously,
φ
−
1
φ(f)
(η
O
B
◦
g)
=
η
B
)
◦
g
=
id
B
◦
g
=
φ
−
1
(η
O
B
◦
(η
O
B
◦
=
f)
=
η
B
◦
f)
=
η
OP
B
f
, i.e.,
φ
−
1
φ
is an identity function and hence
φ
is a
bijection. Let us demonstrate that
K
is a functor.
For any identity arrow
id
T
=
(η
B
◦
)
◦
f
=
id
TB
◦
f
=
A
in
DB
T
we obtain
K
1
(id
T
)
:
−→
=
θ(η
A
)
A
φθ
−
1
(θ(η
A
))
η
O
A
◦
=
φ(η
A
)
=
η
A
=
id
A
(because
η
A
is an isomorphism). For any
two arrows
g
T
:
B
−→
C
and
f
T
:
A
−→
B
in Kleisli category, we obtain
K
1
θ
μ
C
◦
θ
−
1
(f
T
)
K
1
(g
T
◦
Tθ
−
1
(g
T
)
f
T
)
=
◦
from Definition
59
of Kleisli category;
TB
θ
−
1
(g
T
)
θ
−
1
(f
T
)
we introduce
g
:
B
−→
TC
and
f
:
A
−→
φθ
−
1
θ(μ
C
◦
f)
=
φθ
−
1
θ(id
TC
◦
f)
=
φθ
−
1
θ(Tg
f)
=
Tg
◦
Tg
◦
◦