background image

Proposition 33.

It is really a quasi-cartesian situation.

Proof.

We need to prove

ρ

Z

ρ

=

ρ

. Really,

ρZρf

=

ρZ

(

Src

f

;

Dst

f

) =

ρ

(

;

Src

f

;

Dst

f

) = (

Src

f

;

Dst

f

) =

ρf .

Definition 34.

The quasi-cartesian situation of reloids is:

1. Forms are pairs

(

A

;

B

)

of sets.

2. Arguments are reloids.

3. The form of an argument

f

is

(

Src

f

;

Dst

f

)

.

4. Zero of the form

(

A

;

B

)

is

0

RLD

(

A

;

B

)

.

Proposition 35.

It is really a quasi-cartesian situation.

Proof.

We need to prove

ρ

Z

ρ

=

ρ

. Really,

ρZρf

=

ρZ

(

Src

f

;

Dst

f

) =

ρ

0

RLD

(

Src

f

;

Dst

f

)

= (

Src

f

;

Dst

f

) =

ρf .

Next we need to prove that cross-composition product of some particular categories with star-
morphisms are quasi-cartesian functions with injective aggregation.

Theorem 36.

Cross-composition product (for small indexed families of relations) is a quasi-carte-

sian function with injective aggregation from the quasi-cartesian situation

S

0

of binary relations

to the quasi-cartesian situation

S

1

of pointfree funcoids over posets with least elements.

Proof.

First prove that it is a pre-quasi-cartesian function. We need to show that for every small

indexed families

x

,

y

of

Rel

-morphisms:

1.

x

ZC

0

Q

(

C

)

x

=

Z

1

ρ

1

Q

(

C

)

x

;

2.

ρ

0

x

=

ρ

0

y

ρ

1

Q

(

C

)

x

=

ρ

1

Q

(

C

)

y

;

Q

(

C

)

x

=

Z

1

ρ

1

Q

(

C

)

x

Q

(

C

)

x

=

Z

1

(

FCD

(

StarHom

(

λi

dom

x

:

Src

x

i

);

StarHom

(

λi

dom

x

:

Dst

x

i

)))

Q

(

C

)

x

= 0

FCD

(

StarHom

(

λi

dom

x

:

Src

x

i

);

StarHom

(

λi

dom

x

:

Dst

x

i

))

⇔ ∀

a

StarHom

(

λi

dom

x

:

Src

x

i

):

D

Q

(

C

)

x

E

a

= 0

StarHom

(

λi

dom

x

:

Dst

x

i

)

⇔ ∀

a

StarHom

(

λi

dom

x

:

Src

x

i

):

StarComp

(

a

;

x

) = 0

StarHom

(

λi

dom

x

:

Dst

x

i

)

⇔ ∀

a

StarHom

(

λi

dom

x

:

Src

x

i

):

GR StarComp

(

a

;

x

) =

;

a

StarHom

(

λi

dom

x

:

Src

x

i

):

GR StarComp

(

a

;

x

) =

∅ ⇐

x

ZC

0

.

a

StarHom

(

λi

dom

x

:

Src

x

i

):

GR StarComp

(

a

;

x

) =

∅ ⇒

GR StarComp

dom

x

;

Q

i

dom

x

Src

x

i

;

x

=

∅ ⇒

L

arity

a

y

Q

i

dom

x

Src

x

i

i

arity

a

:

y

i

x

i

L

i

¬∀

i

arity

a

L

, y

Src

x

i

:

yx

i

L

⇔ ¬∀

i

arity

a

:

x

i

0

x

ZC

0

.

Thus

x

ZC

0

Q

(

C

)

x

=

Z

1

ρ

1

Q

(

C

)

x

.

If

ρ

0

x

=

ρ

0

y

then arity

x

=

arity

y

=

n

for some index set

n

.

8