 Proposition 10.

f

2

C

(

;

)

,

v

f

y

f

,

f

f

y

v

for every monovalued entirely dened

morphism

f

.

Proposition 11.

[TODO: Check correct usage of these implications below!]

1. Every entirely dened monovalued morphism is metamonovalued and metacomplete.
2. Every surjective injective morphism is metainjective and co-metacomplete.

Proof.

1. Let

f

be an entirely dened monovalued morphism.

(

d

G

)

f

v

d

g

2

G

(

g

f

)

by monotonicity of composition.

Using the fact that

f

is monovalued and entirely dened:

¡

d

g

2

G

(

g

f

)

f

y

v

d

g

2

G

(

g

f

f

y

)

v

d

G

;

d

g

2

G

(

g

f

)

v

¡

d

g

2

G

(

g

f

)

f

y

f

v

(

d

G

)

f

.

So

(

d

G

)

f

=

d

g

2

G

(

g

f

)

.

Let

f

be a entirely dened monovalued morphism.

f

(

F

G

)

w

F

g

2

G

(

f

g

)

by monotonicity of composition.

Using the fact that

f

is entirely dened and monovalued:

f

y

¡F

g

2

G

(

f

g

)

w

F

g

2

G

(

f

y

f

g

)

w

d

G

;

F

g

2

G

(

f

g

)

w

f

f

y

F

g

2

G

(

f

g

)

w

f

(

F

G

)

.

So

f

(

F

G

) =

F

g

2

G

(

f

g

)

.

2. By duality.

3 General product in partially ordered dagger category

To understand the below better, you can restrict your imagination to the case when

C

is the

category Rel.

3.1 Inmum product

Let

C

be a dagger category, each Mor-set of which is a complete lattice (having order agreed with

the dagger).

We will designate some morphisms as

principal

and require that principal morphisms are both

metacomplete and co-metacomplete. (For a particular example of the category Rel, all morphisms
are considered principal.)

Let

Q

(

Q

)

X

be an object for each indexed family

X

of objects.

Let

be a partial function mapping elements

X

2

dom

(which consists of small indexed fam-

ilies of objects of

C

) to indexed families

Q

(

Q

)

X

!

X

i

of principal morphisms (called

projections

)

for every

i

2

dom

X

.

We will denote particular morphisms as

i

X

.

Remark 12.

In some important examples the function

is entire, that is dom

is the set of all

small indexed families of objects of

C

. However there are also some important examples where it

is partial.

Denition 13.

Inmum product

Q

F

(such that

is dened at

j

2

n

:

Src

F

j

and

j

2

n

:

Dst

F

j

)

is dened by the formula

Y

(

L

)

F

=

l

i

2

dom

F

¡

i

j

2

n

:

Dst

F

j

y

F

i

i

j

2

n

:

Src

F

j

:

This formula can be (over)simplied to:

Y

(

L

)

F

=

l

i

2

dom

F

¡¡

i

Dst

F

y

F

i

i

Src

F

:

2

Section 3