 4.3. CATEGORY

REL

62

Obvious

365

.

P

(

P

U, A

) is also a set of typed sets.

Definition

366

.

I will denote

T

U

=

T

P

U

.

Remark

367

.

This means that

T

U

is the set of typed subsets of a set

U

.

Obvious

368

.

T

U

=

n

(

P

U,X

)

X

P

U

o

=

{

P

U

} ×

P

U

=

P

(

P

U, U

).

Obvious

369

.

T

U

is a complete atomistic boolean lattice. Particularly:

1

.

T

U

= (

P

U,

);

2

.

>

T

U

= (

P

U, U

);

3

. (

P

U, A

)

t

(

P

U, B

) = (

P

U, A

B

);

4

. (

P

U, A

)

u

(

P

U, B

) = (

P

U, A

B

);

5

.

d

A

S

(

P

U, A

) = (

P

U,

S

A

S

A

);

6

.

d

A

S

(

P

U, A

) =

P

U,

(

T

A

S

A

if

A

6

=

U

if

A

=

!

;

7

. (

P

U, A

) = (

P

U, U

\

A

);

8

. atomic elements are (

P

U,

{

x

}

) where

x

U

.

Typed sets are “better” than regular sets as (for example) for a set

U

and a typed

set

X

the following are defined by regular order theory:

atoms

X

;

X

;

d

T

U

.

For regular (“non-typed”) sets these are not defined (except of atoms

X

which how-

ever needs a special definition instead of using the standard order-theory definition

of atoms).

Typed sets are convenient to be used together with filters on sets (see below),

because both typed sets and filters have a set

P

U

as their type.

Another advantage of typed sets is that their binary product (as defined below)

is a

Rel

-morphism. This is especially convenient because below defined products

of filters are also morphisms of related categories.

Well, typed sets are also quite awkward, but the proper way of doing modern

mathematics is

type theory

not ZFC, what is however outside of the topic of this

book.

4.3. Category Rel

I remind that

Rel

is the category of (small) binary relations between sets, and

Set

is its subcategory where only monovalued entirely defined morphisms (func-

tions) are considered.

Definition

370

.

Order on

Rel

(

A, B

) is defined by the formula

f

v

g

GR

f

GR

g

.

Obvious

371

.

This order is isomorphic to the natural order of subsets of the

set

A

×

B

.

Definition

372

.

X

[

f

]

Y

GR

X

[GR

f

]

GR

Y

and

h

f

i

X

=

(Dst

f,

h

GR

f

i

GR

X

) for a

Rel

-morphism

f

and typed sets

X

T

Src

f

,

Y

T

Dst

f

.

Definition

373

.

For category

Rel

there is defined reverse morphism:

(

A, B, F

)

1

= (

B, A, F

1

).

Obvious

374

.

(

f

1

)

1

=

f

for every

Rel

-morphism

f

.