Double Category: Prof

Prof is a double category assembled from the categories Prof and Cat. Its objects are categories, its horizontal arrows are functors, its vertical arrows are profunctors, and its squares are natural transformations. 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 Prof to the 2-categories Cat and Prof respectively, augmented with natural transformations for 2-cells:

double_categories: Prof, Cat

This data as json