background image

2.

ρ

x

=

ρ

y

ρ

Q

(

ord

)

x

=

ρ

Q

(

ord

)

y

;

that is

1.

x

ZC

Q

(

ord

)

x

=

Z

arity

Q

(

ord

)

x

;

2. arity

x

=

arity

y

arity

Q

(

ord

)

x

=

arity

Q

(

ord

)

y

;

that is

1.

x

ZC

Q

(

ord

)

x

=

Z

arity

Q

(

ord

)

x

;

2. arity

x

=

arity

y

P

(

arity

x

) =

P

(

arity

y

)

;

but these formulas are obvious.

Next prove that it is a quasi-cartesian function. We need to show that for every indexed family of
sets

 

Y

(

D

)

x

!

|

{

x

X

dom

A

|

ρ

x

=

A

}\

ZC

is injection. This follows from the known fact that

(

Q

x

)

|

{

x

X

dom

A

|

ρ

x

=

A

}\

ZC

is an injection.

[TODO: More detailed proof.]

Definition 30.

The quasi-cartesian situation of pointfree funcoids over posets with least elements

is:

1. Forms are pairs

(

A

;

B

)

of posets with least elements.

2. Arguments are pointfree funcoids.

3. The form of an argument

f

is

(

Src

f

;

Dst

f

)

.

4. Zero of the form

(

A

;

B

)

is

0

FCD

(

A

;

B

)

= (

A

× {

0

B

}

;

B

× {

0

A

}

)

. (It exists because

A

and

B

have least elements.)

Proposition 31.

It is really a quasi-cartesian situation.

Proof.

We need to prove

ρ

Z

ρ

=

ρ

. Really,

ρZρf

=

ρZ

(

Src

f

;

Dst

f

) =

ρ

0

FCD

(

Src

f

;

Dst

f

)

= (

Src

f

;

Dst

f

) =

ρf .

Definition 32.

The quasi-cartesian situation of binary relations is:

1. Forms are pairs

(

A

;

B

)

of sets.

2. Arguments are

Rel

-morphisms;

3. The form of an argument

f

is

(

Src

f

;

Dst

f

)

.

4. Zero of the form

(

A

;

B

)

is the

Rel

-morphism

(

;

A

;

B

)

.

7