 Denition 17.129.

A

quasi-invertible

category with star-morphisms is a quasi-invertible precat-

egory with star-morphisms which is a category with star-morphisms.

Each category with star-morphisms gives rise to a category (

abrupt category

, see a remark

below why I call it abrupt), as described below. Below for simplicity I assume that the set

M

and the set of our indexed families of functions are disjoint. The general case (when they are not
necessarily disjoint) may be easily elaborated by the reader.

Objects are indexed (by arity

m

for some

m

2

M

) families of objects of the category

C

and

an (arbitrarily chosen) object None not in this set.

There are the following disjoint sets of morphisms:

1. indexed (by arity

m

for some

m

2

M

) families of morphisms of

C

;

2. elements of

M

;

3. the identity morphism id

None

on None.

Source and destination of morphisms are dened by the formulas:

Src

f

=

i

2

dom

f

:

Src

f

i

;

Dst

f

=

i

2

dom

f

:

Dst

f

i

;

Src

m

=

None;

Dst

m

=

Obj

m

.

Compositions of morphisms are dened by the formulas:

g

f

=

i

2

dom

f

:

g

i

f

i

for our indexed families

f

and

g

of morphisms;

f

m

=

StarComp

(

m

;

f

)

for

m

2

M

and a composable indexed family

f

;

m

id

None

=

m

for

m

2

M

;

id

None

id

None

=

id

None

.

Identity morphisms for an object

X

are:

i

2

X

:

id

X

i

if

X

=

/

None;

id

None

if

X

=

None.

We need to prove it is really a category.

Proof.

We need to prove:

1. Composition is associative.
2. Composition with identities complies with the identity law.

Really:

1.

(

h

g

)

f

=

i

2

dom

f

: (

h

i

g

i

)

f

i

=

i

2

dom

f

:

h

i

(

g

i

f

i

) =

h

(

g

f

)

;

g

(

f

m

) =

StarComp

(

StarComp

(

m

;

f

);

g

) =

StarComp

(

m

;

i

2

arity

m

:

g

i

f

i

) =

StarComp

(

m

;

g

f

) = (

g

f

)

m

;

f

(

m

id

None

) =

f

m

= (

f

m

)

id

None

.

2.

m

id

None

=

m

; id

Dst

m

m

=

StarComp

(

m

;

i

2

arity

m

:

id

Obj

m

i

) =

m

.

Remark 17.130.

I call the above dened category

abrupt category

because (excluding identity

morphisms) it allows composition with an

m

2

M

only on the left (not on the right) so that the

morphism

m

is abrupt on the right.

By

J

x

0

;

:::

;

x

n

¡

1

K

I denote an

n

-tuple.

Denition 17.131.

Precategory with star morphisms

induced

by a dagger precategory

C

is:

The base category is

C

.

220

Multifuncoids and staroids