 4. PRODUCT

45

thus it is a system of presides.

That this is a bounded system of presides follows from the formulas

(

FCD

)

RLD

(

A,B

)

=

and (

FCD

)

>

RLD

(

A,B

)

=

>

.

It is with identities, because proposition 1168. It is with correct identities by

proposition 898.

FiXme

: Also for pointfree reloids.

FiXme

: These examples works for (dagger) systems of sides with binary prod-

uct.

4. Product

Definition

2268

.

Binary product

of objects of presides with identities is de-

fined by the formula

X

×

Y

= id

Y

◦> ◦

id

X

.

Definition

2269

.

System of presides with identities is

with correct binary

product

when

f

u

(

X

×

Y

) = id

Y

f

id

X

for every preside

f

.

Proposition

2270

.

h

A

×

B

i

X

=

(

if

X

A

B

if

X

6

A

Proof.

h

A

×

B

i

X

=

h

id

B

◦> ◦

id

A

i

X

=

h

id

B

ih>ih

id

A

i

X

=

B

u h>i

(

X

u

A

) =

B

u

(

if

X

A

>

if

X

6

A

=

(

if

X

A

B

if

X

6

A

Definition

2271

.

I will call a system of sides

with correct meet

when

(

X

0

×

Y

0

)

u

(

X

1

×

Y

1

) = (

X

0

u

X

1

)

×

(

Y

0

u

Y

1

)

.

Proposition

2272

.

Faithful systems of presides with identities are with correct

meet.

Proof.

(

X

0

×

Y

0

)

u

(

X

1

×

Y

1

) = id

Y

1

(

X

0

×

Y

0

)

id

X

1

. Thus

h

(

X

0

×

Y

0

)

u

(

X

1

×

Y

1

)

i

P

=

h

id

Y

1

ih

X

0

×

Y

0

ih

id

X

1

i

P

=

h

id

Y

1

i

(

if

X

0

h

id

X

1

i

P

Y

0

if

X

0

6 h

id

X

1

i

P

=

(

if

X

0

u

X

1

P

Y

0

u

Y

1

if

X

0

u

X

1

6

P

=

h

(

X

0

u

X

1

)

×

(

Y

0

u

Y

1

)

i

P.

So (

X

0

×

Y

0

)

u

(

X

1

×

Y

1

) = (

X

0

u

X

1

)

×

(

Y

0

u

Y

1

) follows by full faithfulness.

Proposition

2273

.

Systems of presides with correct identities are with correct

meet.

Proof.

(

X

0

×

Y

0

)

u

(

X

1

×

Y

1

) = id

Y

1

(

X

0

×

Y

0

)

id

X

1

= id

Y

1

(id

Y

0

◦>◦

id

X

0

)

id

X

1

= id

Y

0

u

Y

1

◦> ◦

id

X

0

u

X

1

= (

X

0

u

X

1

)

×

(

Y

0

u

Y

1

).

For some sides holds the formula

f

(

X

×

Y

) =

X

× h

f

i

Y

. I refrain to give a

name for this property.