Rel

Rel is the category of sets and relations.

It is a very simple yet very rich category.

It is used in semantics of linear logic and programming language semantics

Definition

🐣

This section is empty. Feel free to contribute to it!

Properties

Rel is very simple and yet has a lot of structure. Categorically, it is an instance of a:

• symmetric monoidal category, in two different ways (two different monoidal product)
• traced category
• dagger compact category
• It is the prototypal example of allegory

As such, it is a model of MLL.

Rel can be equipped with multiples comonads, such as Fam or Sym, making it the linear category of a co-Kleisli category and thus a model of MELL.

Examples of use

Rel serves as a basis for a lot categorical investigations.

For example, thin spans are a generalisation of Rel + Fam, inspired by concurrent game semantics, that aim to capture a more precise quantitative information on programs, but still without any notion of time, thus avoiding the complicated machinery required in concurrent game semantics.

References

Historical references:

🐣

This section is empty. Feel free to contribute to it!