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:

𝓗(Prof) ≅ Cat
𝓥(Prof) ≅ Prof

double_categories: Prof, Cat

This data as json

vertical_2cat horizontal_2cat 2cells_hr
Prof Cat natural transformations