background image

Pointfree binary relations

Victor Porton

November 24, 2015

Abstract

I define

pointfree binary relations

, a way to describe binary rela-

tions and more general structures without referring to particular “points”
(elements).

In this short article I define

pointfree binary relations

, that is a way

to describe binary relations and more general structures without referring to
particular “points” (elements).

Definition.

Remind that

binary relations

(also called morphisms of the cat-

egory

Rel

) are triples (

A, B, f

) where

A

,

B

are sets and

f

P

(

A

×

B

).

Definition. Endo-relations

are relations of the form (

A, A, f

) for some set

A

and

f

P

(

A

×

A

).

Definition. Isomorphism

between relations

µ

P

(

A

0

×

A

0

) and

ν

P

(

A

1

×

A

1

) is a bijection

f

:

A

1

A

0

such that

ν

=

f

1

µ

f

.

I remind that

precategory

is defined as category without requirement of

existence of identity morphisms.

Definition. Ordered precategory

is a precategory, each Hom-set of which

is a poset, subject to the inequalities

f

0

f

1

g

0

g

1

g

0

f

0

g

1

f

1

.

Definition. Isomorphism

of ordered precategories is a map which is both

precategory isomorphism and order isomorphism.

Definition. System of pointfree relations

is:

an ordered precategory (I call morphisms of which

pointfree (binary)

relations

; the composition is denoted

);

for each Hom-sets two posets:

possible domains

and

possible images

;

domain

dom and

image

im (maps from pointfree relations to possible

domains and possible images of its Hom-set), subject to the inequalities

f

g

dom

f

dom

g

im

f

im

g.

1