Double Category: Rel

Rel is a double category assembled from the categories Rel and Set. Its objects are sets, its horizontal arrows are maps, its vertical arrows are relations, and its squares are subrelation inclusions. As with all double categories, we may transpose horizontal and vertical arrows to obtain another double category.

The horizontal and vertical 2-category functors send Rel to the 2-categories Set and Rel respectively, augmented with subrelation inclusions for 2-cells:

double_categories: Rel, Set

This data as json