19.2. COMPOSITION OF POINTFREE FUNCOIDS

285

Thus

h

f

i

(

i

t

j

) =

h

f

i

i

t h

f

i

j

by separability.

Proposition

1502

.

Let

f

be a pointfree funcoid. Then:

1

.

k

[

f

]

i

t

j

k

[

f

]

i

k

[

f

]

j

for every

i, j

Dst

f

,

k

Src

f

if Dst

f

is a

starrish join-semilattice.

2

.

i

t

j

[

f

]

k

i

[

f

]

k

j

[

f

]

k

for every

i, j

Src

f

,

k

Dst

f

if Src

f

is a

starrish join-semilattice.

Proof.

1

.

k

[

f

]

i

t

j

i

t

j

6 h

f

i

k

i

6 h

f

i

k

j

6 h

f

i

k

k

[

f

]

i

k

[

f

]

j

.

2

Similar.

19.2. Composition of pointfree funcoids

Definition

1503

.

Composition

of pointfree funcoids is defined by the formula

(

B

,

C

, α

2

, β

2

)

(

A

,

B

, α

1

, β

1

) = (

A

,

C

, α

2

α

1

, β

1

β

2

)

.

Definition

1504

.

I will call funcoids

f

and

g

composable

when Dst

f

= Src

g

.

Proposition

1505

.

If

f

,

g

are composable pointfree funcoids then

g

f

is

pointfree funcoid.

Proof.

Let

f

= (

A

,

B

, α

1

, β

1

),

g

= (

B

,

C

, α

2

, β

2

). For every

x, y

A

we have

y

6

(

α

2

α

1

)

x

y

6

α

2

α

1

x

α

1

x

6

β

2

y

x

6

β

1

β

2

y

x

6

(

β

1

β

2

)

y.

So (

A

,

C

, α

2

α

1

, β

1

β

2

) is a pointfree funcoid.

Obvious

1506

.

h

g

f

i

=

h

g

i ◦ h

f

i

for every composable pointfree funcoids

f

and

g

.

Theorem

1507

.

(

g

f

)

1

=

f

1

g

1

for every composable pointfree funcoids

f

and

g

.

Proof.

(

g

f

)

1

=

f

1

g

1

=

f

1

g

1

;

((

g

f

)

1

)

1

=

h

g

f

i

=

(

f

1

g

1

)

1

.

Proposition

1508

.

(

h

g

)

f

=

h

(

g

f

) for every composable pointfree

funcoids

f

,

g

,

h

.

Proof.

h

(

h

g

)

f

i

=

h

h

g

i ◦ h

f

i

=

h

h

i ◦ h

g

i ◦ h

f

i

=

h

h

i ◦ h

g

f

i

=

h

h

(

g

f

)

i

;

((

h

g

)

f

)

1

=

f

1

(

h

g

)

1

=

f

1

g

1

h

1

=

(

g

f

)

1

h

1

=

(

h

(

g

f

))

1

.

Exercise

1509

.

Generalize section

7.4

for pointfree funcoids.