background image

Proof.

??

Galufuncoids

Let

A

and

B

are

Rel

-morphisms. I will denote like

(

A

) =

GR

A

and

(

B

) =

GR

B

.

Definition 9.

Galufuncoids

between

A

and

B

is a quadruple

(

A

;

B

;

α

;

β

)

such that

x

Ob

A

, y

Ob

B

: (

αx

B

y

x

A

βy

)

.

Definition 10.

x

[

f

]

y

x

Src

f

β y

.

Obvious 11.

x

[

f

]

y

x

Src

f

βy

αx

Dst

f

y

.

Remark 12.

Galufuncoids are a generalization of both (pointfree) funcoids and Galois connec-

tions.

Definition 13.

The

reverse

galufuncoid is defined by the formula:

(

A

;

B

;

α

;

β

)

1

= (

B

;

A

;

β

;

α

)

.

Proposition 14.

Composition of (composable) galufuncoids is a galufuncoid.

Proof.

(

α

2

α

1

)

x

y

α

2

α

1

x

y

α

1

x

β

2

y

x

β

1

β

2

y

x

(

β

1

β

2

)

y

.

Obvious 15.

Galufuncoids form a category (similarly to the category of pointfree funcoids).

Definition 16.

On the set of galufuncoids is defined a preorder by the formula:

f

g

[

f

]

[

g

]

.

Galufuncoidal product

Functional galufuncoid

Definition 17.

Functional galufuncoid

ν

/∆

of

ν

through filter

is the endo-galufuncoid defined

by the formulas:

Ob

(

ν

/∆) =

FCD

(

Base

(∆);

Ob

ν

)

h

ν

/∆

i

f

=

ν

f

and

h

(

ν

/∆)

1

i

f

=

ν

1

f

f

Ob

(

ν

/∆)

g

g

1

f

id

FCD

[TODO: Restrict to the special case

f

=

ν

F

to make it

T

2

.]

[TODO:

X

[

SLA

(

f

)]

Y

is defined as existence of

x

X

such that for every entourage of

x

there is

y

Y

which is a subfilter of this entourage.]

Obvious 18.

Ob

(

ν

/∆)

is a symmetric relation.

Proposition 19.

This is really a galufuncoid and

f

[

ν

/∆]

g

g

1

ν

f

id

.

2