 Chapter 17
Multifuncoids and staroids

17.1 Product of two funcoids

17.1.1 Lemmas

Lemma 17.1.

Let

A

,

B

,

C

be sets,

f

2

FCD

(

A

;

B

)

,

g

2

FCD

(

B

;

C

)

,

h

2

FCD

(

A

;

C

)

. Then

g

f

/

h

,

g

/

h

f

¡

1

:

Proof.

Proposition

6.70

.

Lemma 17.2.

Let

A

,

B

,

C

be sets,

f

2

RLD

(

A

;

B

)

,

g

2

RLD

(

B

;

C

)

,

h

2

RLD

(

A

;

C

)

. Then

g

f

/

h

,

g

/

h

f

¡

1

:

Proof.

Theorem

7.16

.

17.1.2 Denition

Denition 17.3.

I will call a

quasi-invertible category

a partially ordered dagger category such

that it holds

g

f

/

h

,

g

/

h

f

y

(17.1)

for every morphisms

f

2

Mor

(

A

;

B

)

,

g

2

Mor

(

B

;

C

)

,

h

2

Mor

(

A

;

C

)

, where

A

,

B

,

C

are objects of

this category.

Inverting this formula, we get

f

y

g

y

/

h

y

,

g

y

/

f

h

y

. After replacement of variables, this

gives:

f

y

g

/

h

,

g

/

f

h

.

As it follows from above, the category of funcoids and the category of reloids are quasi-invertible

(taking

f

y

=

f

¡

1

). Moreover the category of pointfree funcoids between lattices of lters on boolean

lattices is quasi-invertible (theorem

15.63

).

[TODO: Say that Rel is quasi-invertible.]

Exercise 17.1.

Prove that every ordered groupoid is quasi-invertible category if we dene the dagger as the

inverse morphism.

Denition 17.4.

The

cross-composition product

of morphisms

f

and

g

of a quasi-invertible

category is the pointfree funcoid Mor

(

Src

f

;

Src

g

)

!

Mor

(

Dst

f

;

Dst

g

)

dened by the formulas (for

every

a

2

Mor

(

Src

f

;

Src

g

)

and

b

2

Mor

(

Dst

f

;

Dst

g

)

):

f

(

C

)

g

a

=

g

a

f

y

and

¡

f

(

C

)

g

¡

1

b

=

g

y

b

f :

We need to prove that it is really a pointfree funcoid that is that

b

/

f

(

C

)

g

a

,

a

/

¡

f

(

C

)

g

¡

1

b:

This formula means

b

/

g

a

f

y

,

a

/

g

y

b

f

and can be easily proved applying the formula

(

17.1

two times.

203