 Proposition 32.

(

X ÷

A

)

÷

B

=

X ÷

B

if

B

A

.

Proof.

(

X ÷

A

)

÷

B

=

d

{↑

B

(

Y

B

)

|

Y

d

{↑

A

(

X

A

)

|

X

∈ X }}

=

d

{↑

B

(

X

A

)

|

X

X } ⊓ ↑

B

B

=

d

{↑

B

(

X

A

B

)

|

X

∈ X }

=

X ÷

(

A

B

) =

X ÷

B

.

5.2 Category Rel

Category

Rel

with the identity up-arrow functor to itself and “reverse relation” as the dagger is

an obvious example of a partially ordered dagger category under

Rel

.

Definition 33.

f

÷

(

A

×

B

) = (

A

;

B

; (

GR

f

)

÷

(

A

×

B

))

for every

Rel

-morphism

f

.

Proposition 34.

ι

A,B

f

= (

A

;

B

;

GR

f

(

A

×

B

))

.

Proof.

ι

A,B

f

= (

Dst

f

B

)

f

(

A

Src

f

) = (

A

;

B

;

GR

f

(

A

×

B

))

.

5.3 Category

FCD

Category

FCD

with the up-arrow functor

FCD

and “reverse funcoid” as the dagger is a partially

ordered dagger category under

Rel

.

Proposition 35.

A

FCD

B

= (

A

;

B

;

λ

X ∈

F

(

A

):

X ÷

B

;

λ

Y ∈

F

(

B

):

Y ÷

A

)

for objects

A

B

of

FCD

.

Proof.

h

A

FCD

B

iX

=

d

{h

A

FCD

B

i

X

|

X

∈ X }

=

d

{↑

B

h

A

B

i

X

|

X

∈ X }

=

d

{↑

B

(

X

A

B

)

|

X

∈ X }

=

d

{↑

B

(

X

B

)

|

X

∈ X }

=

X ÷

B

.

Rest follows from symmetry.

Proposition 36.

1.

h

A

FCD

B

i

X

=

B

X

for every

X

P

A

if

A

B

.

2.

h

(

B

FCD

A

)

i

Y

=

A

(

Y

A

)

for every

Y

P

B

if

A

B

.

Proof.

By definition of principal funcoid.

5.4 Category

RLD

Category

RLD

with the up-arrow functor

RLD

and “reverse reloid” as the dagger is a partially

ordered dagger category under

Rel

.

Obvious 37.

A

RLD

B

=

RLD

(

A

;

B

)

id

A

B

.

Definition 38.

f

÷

(

A

×

B

) = (

A

;

B

; (

GR

f

)

÷

(

A

×

B

))

for every reloid

f

.

Proposition 39.

ι

A,B

f

=

f

÷

(

A

×

B

)

.

Proof.

ι

A,B

f

= (

Dst

f

RLD

B

)

f

(

A

RLD

Src

f

) =

d

{↑

RLD

((

Dst

f

B

)

F

(

A

Src

f

))

|

F

xyGR

f

}

=

d

{↑

RLD

(

F

(

A

×

B

))

|

F

xyGR

f

}

=

f

÷

(

A

×

B

)

.

[TODO: Filters on cartesian

products vs reloids.]

6 Equalizers

Categories

cont

(

C

)

are defined in .

I will denote

W

the forgetful functor from

cont

(

C

)

to

C

.

In the definition of the category

cont

(

C

)

take values of

as principal morphisms.

[TODO:

Wording.]

4

Section 6