varkor

@ohad The result is far older than that. For instance, the 2-dimensional version already appears in §6.6 of Blackwell–Kelly–Power's 1989 "Two-dimensional monad theory". I don't know what the oldest reference is, but I would imagine it's been known since the 1960s.

@BartoszMilewski@mathstodon.xyz A quick comment: there is no double category of double categories, because distributors between double categories do not compose. (There is, however, a virtual double category of double categories.)

@BartoszMilewski@mathstodon.xyz (Just in case it's not clear why this strict double category Grandis and Paré consider isn't appropriate in this situation, it doesn't have all companions or all conjoints, so doesn't form an equipment.)