such that and , where and denote horizontal and vertical composition of 2-cells.
Given such a companion pair, we say that and are companions of each other.
In the double category of squares (“quintets”) in any 2-category , a companion pair is simply an invertible 2-cell between two parallel 1-morphisms of .
In the double category -Alg of algebras, lax morphisms, and colax morphisms for a 2-monad, an arrow (of either sort) has a companion precisely when it is a strong (= pseudo) -morphism. This is important in the theory of doctrinal adjunction.
The horizontal (or vertical) dual of a companion pair is a conjunction.
Companion pairs (and conjunctions) have a mate correspondence generalizing the calculus of mates in 2-categories.
If every vertical arrow in some double category has a companion, then the functor is a pseudofunctor from the vertical 2-category to the horizontal one, which is the identity on objects, and locally fully faithful by the mate correspondence. A choice of companions that make this a strict 2-functor is called a connection on (an arbitrary choice of companions may be called a “pseudo-connection”). A double category with a connection is thereby equivalent to an F-category. If every vertical arrow also has a conjoint, then this makes into a proarrow equipment, or equivalently a framed bicategory.
Companion pairs and mate-pairs of 2-cells between them in any double category form a 2-category . The functor is right adjoint to the functor sending a 2-category to its double category of squares.