Saying that “a 2-pullback is a 2-limit over a cospan” is in fact a sufficient definition, but we can simplify it and make it more explicit.
A -pullback in a 2-category is a square
which commutes up to isomorphism, and which is universal among such squares in a 2-categorical sense. This means that (1) given any other such square
which commutes up to isomorphism, there exists a morphism and isomorphisms and which are coherent with the given ones above, and (2) given any two morphisms and 2-cells and such that (modulo the given isomorphism ), there exists a unique 2-cell such that and .
The simplification in the above explicit definition has to do with the omission of an unnecessary structure map. Note that an ordinary pullback of comes equipped with maps , , and , but since and , the map is superfluous data and is usually omitted. In the 2-categorical case, where identities are replaced by isomorphisms, it is, strictly speaking, different to give merely and with an isomorphism , than to give , , and with isomorphisms and . However, when 2-limits are considered as only defined up to equivalence (as is the default on the nLab), the two resulting notions of “2-pullback” are the same. In much of the 2-categorical literature, the version with specified would be called a bipullback and the version with not specified would be called a bi-iso-comma-object.
The unsimplified definition would be: a -pullback in a 2-category is a diagram
in which each triangle commutes up to isomorphism, and which is universal among such squares in a 2-categorical sense. This means that (1) given any other such square
in which the triangles commute up to isomorphism, there exists a morphism and isomorphisms and which are coherent with the given ones above, and (2) given any two morphisms and 2-cells and such that (modulo the given isomorphism ), there exists a unique 2-cell such that and .
Stephan: I would not write since 1-cells are not composable with 2-cells.
Toby: They are, through the operation of whiskering.
Stephan: Thank you Toby. I inserted this example in horizontal composition
To see that these definitions are equivalent, we observe that both assert the representability of some 2-functor (where “representability” is understood in the 2-categorical “up-to-equivalence” sense), and that the corresponding 2-functors are equivalent.
We have a canonical pseudonatural transformation that forgets and sets . This is easily seen to be an equivalence, so that any representing object for is also a representing object for and conversely. (Note, though, that in order to define an inverse equivalence we must choose whether to define or .)
2-pullbacks can also be identified with homotopy pullbacks, when the latter are interpreted in -enriched homotopy theory.
If we are in a strict 2-category and all the coherence isomorphisms (, , , etc.) are required to be identities, and in property (1) is required to be unique, then we obtain the notion of a strict 2-pullback. This is an example of a strict 2-limit. Note that since we must have , the two definitions above are still the same. In fact, they are now even isomorphic (and determined up to isomorphism, rather than equivalence).
In literature where “2-limit” means “strict 2-limit,” of course “2-pullback” means “strict 2-pullback.”
Obviously not every 2-pullback is a strict 2-pullback, but also not every strict 2-pullback is a 2-pullback, although the latter is true if either or is an isofibration (and in particular if either is a Grothendieck fibration). A strict 2-pullback is, in particular, an ordinary pullback in the underlying 1-category of our strict 2-category, but it has a stronger universal property than this, referring to 2-cells as well (namely, part (2) of the explicit definition).
If the coherence isomorphisms , , in the squares are retained, but in (1) the isomorphisms and are required to be identities and is required to be unique, then the simplified definition becomes that of a strict iso-comma object, while the unsimplified definition becomes that of a strict pseudo-pullback. (Iso-comma objects are so named because if the isomorphisms in the squares are then replaced by mere morphisms, we obtain the notion of (strict) comma object).
Every strict iso-comma object, and every strict pseudo-pullback, is also a (non-strict) 2-pullback. In particular, if strict iso-comma objects and strict pseudo-pullbacks both exist, they are equivalent, but they are not isomorphic. (Note that their strict universal property determines them up to isomorphism, not just equivalence.) In many strict 2-categories, such as Cat, 2-pullbacks can naturally be constructed as either strict iso-comma objects or strict pseudo-pullbacks.
Replacing the isomorphism in the simplified definition by a mere transformation results in a comma object, while replacing and in the unsimplified definition by mere transformations results in a lax pullback. In a (2,1)-category, any comma object or lax pullback is also a 2-pullback, but this is not true in a general 2-category. Note that comma objects are often misleadingly called lax pullbacks.