UC Riverside

Category theory is known as a language of mathematics. The basic concepts of the language are systematized in a fibrant double category, a two-dimensional structure also known as a bicategory equipped with proarrows.

We give a new definition of the structure: a bifibrant double category is a "two-sided bifibration'' from a category to itself, with a weak composition and identity. We construct the three-dimensional category of bifibrant double categories.

A category forms a bifibrant double category, by forming the union of the arrow double category with its opposite; we call this the weave double category. Then a two-sided bifibration or matrix category is a span of categories which forms a bimodule of weave double categories. These form a three-dimensional category: the objects are categories; the three kinds of morphism are functor, profunctor, and matrix category; the three kinds of square are transformation, matrix functor, and matrix profunctor, and the cubes are matrix transformations. This structure is a "bifibrant triple category without interchange'', which we call a metalogic.

A bifibrant double category is then a pseudomonad in the metalogic of matrix categories; this defines the objects of a three-dimensional construction: a double functor is a morphism of pseudomonads, a vertical profunctor is a ``vertical monad'' between pseudomonads, and a horizontal profunctor is a bimodule of pseudomonads; a vertical transformation is a morphism of vertical monads, a horizontal transformation is a morphism of bimodules, and a double profunctor is a bimodule of vertical monads. A double transformation is a transformation of vertical bimodules. These form the metalogic of bifibrant double categories.