2-natural transformation?
homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
n-category = (n,n)-category
n-groupoid = (n,0)-category
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\colon A\to B$ be a vertical arrow (morphism) and $f\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
such that $\psi \circ_h \phi = id_f$ and $\phi \circ_v \psi = id_{f'}$, where $\circ_h$ and $\circ_v$ denote horizontal and vertical composition of 2-cells.
Given such a companion pair, we say that $f$ and $f'$ are companions of each other.
In the double category $\mathbf{Sq}(K)$ of squares (“quintets”) in any 2-category $K$, a companion pair is simply an invertible 2-cell between two parallel 1-morphisms of $K$.
In the double category $T$-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) $T$-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 $D$ has a companion, then the functor $f\mapsto f'$ is a pseudofunctor $V 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 $D$ (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 $D$ into a proarrow equipment, or equivalently a framed bicategory.
Companion pairs and mate-pairs of 2-cells between them in any double category $D$ form a 2-category $Comp(D)$. The functor $Comp\colon DblCat \to 2Cat$ is right adjoint to the functor $Sq\colon 2Cat \to DblCat$ sending a 2-category to its double category of squares.
Marco Grandis and Robert Pare, Adjoints for double categories
Robert Dawson? and Robert Pare and Dorette Pronk, The Span construction, TAC.
Michael Shulman, Framed bicategories and monoidal fibrations, TAC