 19.9. CATEGORY OF POINTFREE FUNCOIDS

301

Proposition

1569

.

Let

A

be a meet-semilattice with least element and

B

be

a poset with least element. If

a

is an atom of

A

,

f

pFCD

(

A

,

B

) then

f

|

a

=

a

×

FCD

h

f

i

a

.

Proof.

Let

X ∈

A

.

X u

a

6

=

A

⇒ h

f

|

a

iX

=

h

f

i

a,

X u

a

=

A

⇒ h

f

|

a

iX

=

B

.

Proposition

1570

.

f

(

A ×

FCD

B

) =

A ×

FCD

h

f

iB

for elements

A ∈

A

and

B

B

of some posets

A

,

B

,

C

with least elements and

f

pFCD

(

B

,

C

).

Proof.

Let

X ∈

A

,

Y ∈

B

.

f

(

A ×

FCD

B

)

X

=

(

h

f

iB

if

X 6 A

if

X  A

!

=

A ×

FCD

h

f

iB

X

;

(

f

(

A ×

FCD

B

))

1

Y

=

(

B ×

FCD

A

)

f

1

Y

=

(

A

if

f

1

Y 6 B

if

f

1

Y  B

!

=

(

A

if

Y 6 h

f

iB

if

Y  h

f

iB

!

=

h

f

iB ×

FCD

A

Y

=

(

A ×

FCD

h

f

iB

)

1

Y

.

19.9. Category of pointfree funcoids

I will define the category

pFCD

of pointfree funcoids:

The class of objects are small posets.

The set of morphisms from

A

to

B

is

pFCD

(

A

,

B

).

The composition is the composition of pointfree funcoids.

Identity morphism for an object

A

is (

A

,

A

,

id

A

,

id

A

).

To prove that it is really a category is trivial.

The

category of pointfree funcoid quintuples

is defined as follows:

Objects are pairs (

A

,

A

) where

A

is a small meet-semilattice and

A ∈

A

.

The morphisms from an object (

A

,

A

) to an object (

B

,

B

) are tuples

(

A

,

B

,

A

,

B

, f

) where

f

pFCD

(

A

,

B

) and

x

A

:

h

f

i

x

v A

,

y

B

:

f

1

y

v B

.

(28)

The composition is defined by the formula

(

B

,

C

,

B

,

C

, g

)

(

A

,

B

,

A

,

B

, f

) = (

A

,

C

,

A

,

C

, g

f

)

.

Identity morphism for an object (

A

,

A

) is id

pFCD

(

A

)

A

. (Note: this is defined

only for meet-semilattices.)

To prove that it is really a category is trivial.

Proposition

1571

.

For strongly separated and bounded

A

and

B

formula (

28

)

is equivalent to each of the following:

1

. dom

f

v A ∧

im

f

v B

;

2

.

f

v A ×

FCD

B

.

Proof.

Because

h

f

i

x

v

im

f

,

f

1

y

v

dom

f

, and theorem

1558

.