background image

is defined as a staroid

q

B

=

pStrd

(

λi

dom

f

:

RLD

(

Src

f

i

;

Src

g

i

))

such that

q

=

(

B

;

C

;

B

)

(

A

;

C

;

A

)

p

where

C

=

pStrd

Q

i

dom

f

Src

f

i

;

Q

i

dom

f

Dst

f

i

.

Definition 68.

We will define

displaced product

of a family

f

of funcoids by the formula:

Q

(

DP

)

f

=

DP

Q

(

C

)

f

.

Remark 69.

The interesting aspect of displaced product of funcoids is that displaced product of

pointfree funcoids is a funcoid (not just a pointfree funcoid).

7 Multifuncoids

Definition 70.

I call an

pre-multifuncoid sketch

f

of the form

A

(where every

A

i

is a poset) the

pair

(

A

;

α

)

where for every

i

dom

α

α

i

:

Y

A

|

(

dom

A

)

\{

i

}

A

i

.

I denote

h

f

i

=

α

.

Definition 71.

A pre-multifuncoid sketch

on powersets

is a pre-multifuncoid sketch such that

every

A

i

is the set of filters on a powerset.

Definition 72.

I will call a

pre-multifuncoid

a pre-multifuncoid sketch such that for every

i,

j

dom

A

and

L

Q

A

L

i

α

i

L

|

(

dom

L

)

\{

i

}

L

j

α

j

L

|

(

dom

L

)

\{

j

}

.

(4)

Definition 73.

Let

A

is an indexed family of starrish posets. The pre-staroid

corresponding

to a

pre-multifuncoid

f

is

[

f

]

defined by the formula:

form

[

f

]=

A

and

L

GR

[

f

]

L

i

h

f

i

i

L

|

(

dom

L

)

\{

i

}

.

Proposition 74.

The pre-staroid corresponding to a pre-multifuncoid is really a pre-staroid.

Proof.

By the definition of starrish posets.

Definition 75.

I will call a

multifuncoid

a pre-multifuncoid to which corresponds a staroid.

Definition 76.

I will call a

completary multifuncoid

a pre-multifuncoid to which corresponds a

completary staroid.

Theorem 77.

Fix some indexed family

A

of boolean lattices. The the set of multifuncoids

g

bijectively corresponds to set of pre-staroids

f

of form

A

by the formulas:

1.

f

= [

g

]

for every

i

dom

A

,

L

Q

A

;

2.

h

g

i

i

L

= (

val

f

)

i

L.

Proof.

Let

f

is a pre-staroid of the form

A

. If

α

is defined by the formula

α

i

L

=

h

f

i

i

L

then

∂α

i

L

= (

val

f

)

i

L

. Then

L

i

α

i

L

|

(

dom

L

)

\{

i

}

L

f

L

j

α

j

L

|

(

dom

L

)

\{

j

}

.

For the staroid

f

defined by the formula

L

f

L

i

α

i

L

|

(

dom

L

)

\{

i

}

we have:

L

f

L

i

∂α

i

L

|

(

dom

L

)

\{

i

}

L

i

(

val

f

)

i

L

|

(

dom

L

)

\{

i

}

L

f

;

Multifuncoids

9