nLab companion pair

Companion pairs


2-Category theory

Higher category theory

higher category theory

Basic concepts

Basic theorems





Universal constructions

Extra properties and structure

1-categorical presentations

Companion pairs


A companion pair in a double category is a way of saying that a horizontal morphism and a vertical morphism are “isomorphic”, even though they do not live in the same 1-category/2-category.


Let f:ABf\colon A\to B be a vertical arrow (morphism) and f:ABf'\colon A\to B a horizontal arrow in a double category. These arrows are said to be a companion pair if they come equipped with 2-cells

A f B f ϕ id B id BandA id A id ψ f A f B \array{ A & \overset{f'}{\to} & B \\ ^f\downarrow & ^{\phi}\swArrow & \downarrow^{id} \\ B & \underset{id}{\to} & B} \qquad and\qquad \array{ A & \overset{id}{\to} & A \\ ^{id} \downarrow & ^{\psi}\swArrow & \downarrow^f \\ A & \underset{f'}{\to} & B }

such that ϕ hψ=id f\phi \circ_h \psi = id_{f'} and ϕ vψ=id f\phi \circ_v \psi = id_{f}, where h\circ_h and v\circ_v denote horizontal and vertical composition of 2-cells.

Given such a companion pair, we say that ff and ff' are companions of each other.



  • 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 DD has a companion, then the functor fff\mapsto f' is a pseudofunctor VDHDV D\to H D 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 DD (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 DD into a proarrow equipment, or equivalently a framed bicategory.

  • Companion pairs and mate-pairs of 2-cells between them in any double category DD form a 2-category Comp(D)Comp(D). The functor Comp:DblCat2CatComp\colon DblCat \to 2Cat is right adjoint to the functor Sq:2CatDblCatSq\colon 2Cat \to DblCat sending a 2-category to its double category of squares.


Last revised on June 22, 2023 at 19:42:26. See the history of this page for a list of all contributions to it.