Remark 126.

h

χf

i

= (

f

◦ −

)

is the Hom-functor Hom

(

f ,

)

and we can apply Yoneda lemma to it.

Obvious 127.

h

χ

(

g

f

)

i

a

=

g

f

a

for composable morphisms

f

and

g

or a quasi-invertible

category.

11.2 General cross-composition

Let fix a quasi-invertible category with with star-morphisms. If

f

is an indexed family of morphisms

from its base category, then the pointfree funcoid

Q

(

C

)

f

from StarHom

(

λi

dom

f

:

Src

f

i

)

to

StarHom

(

λi

dom

f

:

Dst

f

i

)

is defined by the formulas (for all star-morphisms

a

and

b

of these

forms):

*

Y

(

C

)

f

+

a

=

StarComp

(

a

;

f

)

and

Y

(

C

)

f

!

1

+

b

=

StarComp

(

b

;

f

)

.

It is really a pointfree funcoid by the definition of quasi-invertible category.

In the terms of abrupt categories, these formulas can be rewritten as:

Y

(

C

)

f

=

χf .

Theorem 128.

Q

(

C

)

g

Q

(

C

)

f

=

Q

i

n

(

C

)

(

g

i

f

i

)

for every

n

-indexed families

f

and

g

of

composable morphisms of a quasi-invertible category with star-morphisms.

Proof.

D

Q

i

n

(

C

)

(

g

i

f

i

)

E

a

=

StarComp

(

a

;

λi

n

:

g

i

f

i

) =

StarComp

(

StarComp

(

a

;

f

);

g

)

and

D

Q

(

C

)

g

Q

(

C

)

f

E

a

=

D

Q

(

C

)

g

ED

Q

(

C

)

f

E

a

=

StarComp

(

StarComp

(

a

;

f

);

g

)

.

Corollary 129.

Q

(

C

)

f

k

1

Q

(

C

)

f

0

=

Q

i

n

(

C

)

(

f

i

(

k

1)

f

i

(

k

))

for every

n

-indexed

families

f

0

,

, f

n

1

,

g

0

,

, g

n

1

composable morphisms of a quasi-invertible category with star-

morphisms.

Proof.

By math induction.

11.3 Some properties of staroids

Lemma 130.

Let

A

0

, A

1

(

P

)

n

are two families of sets and

δ

P

((

P

)

n

)

. Then

δ

Y

i

n

(

A

0

i

A

1

i

)

∅ ⇔ ∃

c

∈ {

0

,

1

}

n

:

δ

Y

i

n

A

c

(

i

)

i

.

Proof.

f

Q

i

n

(

A

0

i

A

1

i

)

⇔ ∀

i

n

: (

f

i

A

0

i

A

1

i

)

⇔ ∀

i

n

: (

f

i

A

0

i

f

i

A

1

i

)

⇔ ∃

c

∈ {

0

,

1

}

n

i

n

:

f

i

A

c

(

i

)

i

⇔ ∃

c

∈ {

0

,

1

}

n

:

f

Q

i

n

A

c

(

i

)

i

.

f

δ

Q

i

n

(

A

0

i

A

1

i

)

f

δ

∧ ∃

c

∈ {

0

,

1

}

n

:

f

Q

i

n

A

c

(

i

)

i

⇔ ∃

c

∈ {

0

,

1

}

n

:

f

δ

Q

i

n

A

c

(

i

)

i

⇒ ∃

c

∈ {

0

,

1

}

n

:

δ

Q

i

n

A

c

(

i

)

i

. The reverse implication is obvious.

Theorem 131.

Let

A

=

A

i

n

is a family of boolean lattices.

A relation

δ

P

Q

atoms

F

(

A

i

)

such that for every

a

Q

atoms

F

(

A

i

)

A

a

:

δ

Y

i

n

atoms

A

i

A

i

∅ ⇒

a

δ

(5)

can be continued till the function

f

for a unique staroid

f

of the form

λi

n

:

P

(

A

i

)

. The funcoid

f

is completary.

For every

X ∈

Q

i

n

F

(

A

i

)

X ∈

GR

f

δ

Y

i

n

atoms

X

i

.

(6)

Product of an arbitrary number of funcoids

19