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)
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 )
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
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
Search WWH ::




Custom Search