Category of relations as monoidal category

Stream: Is there code for X?

[Martin Biehl]

I would like to implement a monoidal functor (I think it's basically what is called the contravariant power set functor) from $\mathbf{Rel}$ to $\mathbf{Cat}$ (or to the category $\mathbf{PreOrd}$ of preorders and monotone functions).
For this I need definitions of $\mathbf{Rel}$ as a monoidal category (with Cartesian product as monoidal product), and $\mathbf{Cat}$ (seems to be implemented in mathlib4 here) or $\mathbf{PreOrd}$, and finally of the monoidal functor.

I am new to lean so I have a dumb initial question:

• Is this a easy thing to do or is this maybe hard for some reason? Or something in between?

More particularly:

• Is $\mathbf{Rel}$ with the Cartesian product as the monoidal product implemented somewhere?

• If not, is it a reasonable approach to start with RelCat from mathlib4 and turn it into a monoidal category maybe by using OfChosenFiniteProducts? Or is there a better way?

• Would it make things a lot easier if I restricted myself to the category of finite sets and relations? I could do that for my usecase I think.

[Joël Riou]

Martin Biehl said:

$\mathbf{Cat}$ (seems to be implemented in mathlib4 here)

We do not have the monoidal structure on Cat, but it would be nice to use the results in the folder Mathlib.CategoryTheory.Products.