Comparing loose bimodules and double barrels using pseudo-models of enhanced sketches

TL;DR

This paper explores the concept of bimodules between double categories in the loose direction, providing two equivalent formulations and introducing pseudo-models of enhanced sketches to facilitate the theory of loose bimodules.

Contribution

It introduces two equivalent formulations of loose bimodules between double categories and defines pseudo-models of enhanced sketches, advancing the understanding of double category theory.

Findings

Two formulations of loose bimodules are proven equivalent.

Pseudo-models of enhanced sketches are introduced and shown useful.

The theory of loose bimodules enables new results in double category theory.

Abstract

(Pseudo) double categories have two sorts of morphisms: tight ones which compose strictly, and loose ones which compose up to coherent isomorphism. In this paper, we consider bimodules between double categories in the loose direction. We provide two formulation of this concept -- first as pseudo-bimodules between pseudo-categories in the 2-category of categories, and second as double barrels generalizing Joyal's definition of bimodules between categories as functors into the walking arrow -- and prove these two formulations equivalent. In order to prove this equivalence, we define a notion of \emph{pseudo-model} of an enhanced sketch, which may be of independent interest. We then consider some double category theory unlocked by the theory of loose bimodules: loose adjunctions, and loose limits.