7.3. FUNCOID AS CONTINUATION

147

7.2.1. Composition of funcoids.

Definition

818

.

Funcoids

f

and

g

are

composable

when Dst

f

= Src

g

.

Definition

819

.

Composition

of composable funcoids is defined by the formula

(

B, C, α

2

, β

2

)

(

A, B, α

1

, β

1

) = (

A, C, α

2

α

1

, β

1

β

2

)

.

Proposition

820

.

If

f

,

g

are composable funcoids then

g

f

is a funcoid.

Proof.

Let

f

= (

A, B, α

1

, β

1

),

g

= (

B, C, α

2

, β

2

). For every

X ∈

F

(

A

),

Y ∈

F

(

C

) 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 funcoid.

Obvious

821

.

h

g

f

i

=

h

g

i ◦ h

f

i

for every composable funcoids

f

and

g

.

Proposition

822

.

(

h

g

)

f

=

h

(

g

f

) for every composable 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

i ◦ h

f

i

) =

h

h

i ◦ h

g

f

i

=

h

h

(

g

f

)

i

.

Theorem

823

.

(

g

f

)

1

=

f

1

g

1

for every composable funcoids

f

and

g

.

Proof.

(

g

f

)

1

=

f

1

g

1

=

f

1

g

1

.

7.3. Funcoid as continuation

Let

f

be a funcoid.

Definition

824

.

h

f

i

is the function

T

(Src

f

)

F

(Dst

f

) defined by the

formula

h

f

i

X

=

h

f

i ↑

X.

Definition

825

.

[

f

]

is the relation between

T

(Src

f

) and

T

(Dst

f

) defined

by the formula

X

[

f

]

Y

⇔↑

X

[

f

]

Y.

Obvious

826

.

1

.

h

f

i

=

h

f

i◦ ↑

;

2

. [

f

]

=

1

[

f

]

◦ ↑

.

Obvious

827

.

h

g

ih

f

i

X

=

h

g

f

i

X

for every

X

T

(Src

f

).

Theorem

828

.

For every funcoid

f

and

X ∈

F

(Src

f

),

Y ∈

F

(Dst

f

)

1

.

h

f

iX

=

d

h

f

i

up

X

;

2

.

X

[

f

]

Y ⇔ ∀

X

up

X

, Y

up

Y

:

X

[

f

]

Y

.

Proof.