background image

Remark 122.

We can carry definitions (such as below defined cross-composition product) from

categories with star-morphisms into plain dagger categories. This allows us to research properties
of cross-composition product of indexed families of morphism for categories with star-morphisms
without separately considering the special case of dagger categories and just binary star-composi-
tion product.

10.1 Abrupt of quasi-invertible categories with star-morphisms

Definition 123.

The abrupt partially ordered pre-category of a partially ordered pre-category

with star-morphisms is the abrupt pre-category with the following order of morphisms:

Indexed (by arity

m

for some

m

M

) families of morphisms of

C

are ordered as function

spaces of posets.

Star-morphisms (which are morphisms None

Obj

m

for some

m

M

) are ordered in the

same order as in the pre-category with star-morphisms.

Morphisms None

None which are only the identity morphism ordered by the unique order

on this one-element set.

We need to prove it is a partially ordered pre-category.

Proof.

It trivally follows from the definition of partially ordered pre-category with star-mor-

phisms.

Theorem 124.

When a pre-category with star-morphisms is quasi-invertible, the corresponding

abrupt category is also quasi-invertible.

Proof.

We need to prove:

g

f

h

g

h

f

(or equivalently

f

g

h

g

f

h

) for all kinds

of morphisms.

Consider the cases:

g

=

id

None

.

Subcases:

g

=

h

=

id

None

.

Trivial.

g

M

.

g

f

h

g

h

g

h

f

.

g

M

.

f

g

h

StarComp

(

g

;

f

)

h

g

StarComp

(

h

;

f

)

g

f

h

.

g

is a family of morphism of

C

.

f

g

h

⇔ ∃

i

dom

g

:

f

i

g

i

h

i

⇔ ∃

i

dom

g

:

g

i

f

i

h

i

g

f

h

.

11 Product of an arbitrary number of funcoids

In this section it will be defined a product of an arbitrary (possibly infinite) family of funcoids.

11.1 Mapping a morphism into a pointfree funcoid

Definition 125.

Let’s define the pointfree funcoid

χf

for every morphism

f

or a quasi-invertible

category:

h

χf

i

a

=

f

a

and

h

(

χf

)

1

i

b

=

f

b.

We need to prove it is really a pointfree funcoid.

Proof.

b

h

χf

i

a

b

f

a

a

f

b

a

h

(

χf

)

1

i

b

.

18

Section 11