 6.7. CATEGORIES OF FUNCOIDS

110

Theorem

628

.

im

f

=

d

h

im

i

up

f

and dom

f

=

d

h

dom

i

up

f

for every fun-

coid

f

.

Proof.

im

f

=

h

f

i>

F

(Src

f

)

=

l

h

F

i>

F

(Src

f

)

F

up

f

=

l

im

F

F

up

f

=

l

h

im

i

up

f.

The second formula follows from symmetry.

Proposition

629

.

For every composable funcoids

f

,

g

:

1

. If im

f

w

dom

g

then im(

g

f

) = im

g

.

2

. If im

f

v

dom

g

then dom(

g

f

) = dom

f

.

Proof.

1

.

im(

g

f

) =

h

g

f

i>

F

(Src

f

)

=

h

g

ih

f

i>

F

(Src

f

)

=

h

g

i

im

f

=

h

g

i

(im

f

u

dom

g

) =

h

g

i

dom

g

=

h

g

i>

F

(Src

g

)

=

im

g.

2

dom(

g

f

) = im(

f

1

g

1

) what by proved above is equal to im

f

1

that

is dom

f

.

Lemma

630

.

λ

B ∈

F

(

B

) :

>

F

×

FCD

B

is an upper adjoint of

λf

FCD

(

A

;

B

) :

im

f

(for every sets

A

,

B

).

Proof.

We need to prove im

f

v B ⇔

f

v >

F

×

FCD

B

what is obvious.

Corollary

631

.

Image and domain of funcoids preserve joins.

Proof.

By properties of Galois connections and duality.

6.7. Categories of funcoids

I will define two categories, the

category of funcoids

and the

category of funcoid

triples

.

The

category of funcoids

is defined as follows:

Objects are small sets.

The set of morphisms from a set

A

to a set

B

is

FCD

(

A

;

B

).

The composition is the composition of funcoids.

Identity morphism for a set is the identity funcoid for that set.