Double Category: Lex

Lex is a double category assembled from the categories Lex and Topos. Its objects are finitely complete categories or topoi, its horizontal arrows are geometric arrows, its vertical arrows are left exact functors, 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 Lex to the 2-categories Topos and Lex respectively, augmented with natural transformations for 2-cells:

double_categories: Lex, Topos

This data as json