background image

Star-morphisms are morphisms of

C

.

arity

f

=

f

0

;

1

g

.

Obj

m

=

J

Src

m

;

Dst

m

K

.

StarComp

(

m

;

J

f

;

g

K

) =

g

m

f

y

.

Let prove it is really a precategory with star-morphisms.

Proof.

We need to prove the associativity law:

StarComp

(

StarComp

(

m

;

J

f

;

g

K

);

J

p

;

q

K

) =

StarComp

(

m

;

J

p

f

;

q

g

K

)

:

Really,

StarComp

(

StarComp

(

m

;

J

f

;

g

K

);

J

p

;

q

K

) =

StarComp

(

g

m

f

y

;

J

p

;

q

K

) =

q

g

m

f

y

p

y

=

q

g

m

(

p

f

)

y

=

StarComp

(

m

;

J

p

f

;

q

g

K

)

:

Denition 17.132.

Category with star morphisms

induced

by a dagger category

C

is the above

dened precategory with star-morphisms.

That it is a category (the law of composition with identity) is trivial.

Remark 17.133.

We can carry denitions (such as below dened 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 morphisms for categories with star-morphisms
without separately considering the special case of dagger categories and just binary star-composi-
tion product.

17.10.1 Abrupt of quasi-invertible categories with star-morphisms

Denition 17.134.

The abrupt partially ordered precategory of a partially ordered precategory

with star-morphisms is the abrupt precategory with the following order of morphisms:

Indexed (by arity

m

for some

m

2

M

) families of morphisms of

C

are ordered as function

spaces of posets.

Star-morphisms (which are morphisms None

!

Obj

m

for some

m

2

M

) are ordered in the

same order as in the precategory 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 precategory.

Proof.

It trivially follows from the denition of partially ordered precategory with star-mor-

phisms.

17.11 Product of an arbitrary number of funcoids

In this section it will be dened a product of an arbitrary (possibly innite) indexed family of
funcoids.

17.11.1 Mapping a morphism into a pointfree funcoid

Denition 17.135.

Let's dene 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

y

b:

17.11 Product of an arbitrary number of funcoids

221