 Proof.

Take

P 2

GR

F

from the previous counter-example. We have

8

a

2

Y

i

2

dom

F

atoms

P

i

:

a

2

/

GR

P

:

Take

k

= 1

.

Let

L

=

P j

(

dom

F

)

nf

k

g

. Then

a

2

/

GR

"

F

and thus

a

k

h

"

F

i

k

a

j

(

dom

F

)

nf

k

g

.

Consequently

P

k

h

"

F

i

k

a

j

(

dom

F

)

nf

k

g

and thus

P

k

F

a

2

Q

i

2

(

dom

F

)

nf

k

g

atoms

L

i

F

h

"

F

i

k

a

because

P

k

is principal.

But

P

k

/

h

"

F

i

k

L

. Thus follows

h

"

F

i

k

L

=

/

F

a

2

Q

i

2

(

dom

F

)

nf

k

g

atoms

L

i

F

h

"

F

i

k

a

.

cross-composition-funcoids.tm
Multifuncoid is a function

distributive over join of every single argument? (It seem that no).

6 Typed sets

Use typed sets instead of sets.

Denition 15.

Typed set

is a pair

(

U

;

A

)

of a set

U

and its subset

A

. But we should go more

general: We can dene

typed element

as a pair

(

A

;

a

)

where

A

is a poset and

a

2

A

. Note that

cartesian product can be dened for the special case if it is a powerset.

Remark 16.

Typed sets

is an awkward formalization of type theory sets in ZFC (

U

is meant to

express the

type

of the set). This book could be better written using type theory instead of ZFC,

but I want my book to be understandable for everyone knowing ZFC.

Denition 17.

P

(

U

;

A

) =

f

(

U

;

X

)

j

X

2

P

A

g

.

For typed sets dene order, binary cartesian product (into the category Rel).
Dene typed elements?

T

A

=

f

(

A

;

X

)

j

X

2

P

A

g

=

f

A

P

A

TA

=

f

(

A

;

a

)

j

a

2

A

g

=

f

A

A

Consider typed sets denoted

?

T

A

and

>

T

A

. (It is consistent with

?

F

A

and

>

𝔉

A

.)

h

f

i

and

[

f

]

should be dened for typed sets, not sets.

We shall consider a primary ltrator

(

F

A

;

T

A

)

for every set

A

to dene funcoids and reloids.

Notwithstanding the above, funcoids and reloids are dened between sets, not typed sets.

7 Other

Generalization of down-aligned (and up-aligned): A ltrator

(

A

;

Z

)

is down-closed if

8

a

2

A

9

b

2

Z

:

b

v

a

.

Funcoids can be alternatively dened as:

Y

/

h

f

i

X

,

X

/

h

f

¡

1

i

Y

where

h

f

i

:

A

!

F

(

B

)

and

h

f

¡

1

i

:

B

!

F

(

A

)

.

For a binary relation

f

replace

h

f

i

with

h

f

i

for clarity of notation.

0

! ?

,

1

! >

.

up

(

A

;

Z

)

!

up

A

.

Dene

F

X

2

S

F

(

X

) =

F

f

F

(

X

)

j

X

2

S

g

(with index of the operator symbol).

Proposition 18.34 - dene what is

X

.

Use explicit

p

FCD

to denote pointfree funcoids.

I overcomplicated the denition of

image

for pointfree funcoids. It should be just

h

f

i>

(because

it is used exclusively this way). Is there any single reason to dene it in this general complicated
way? it seems there is none. Also prove im

f

=

max

hh

f

ii

Src

f

.

Theorem 18.

For a diagram to be commutative, it's enough if each simple cycle commutes. See

https://en.wikipedia.org/wiki/Cycle_%28graph_theory%29 for a denition of simple cycles.

4

Section 7