Where can I find an explicit description of the pseudocolimit of a small pseudofunctor to Cat?

Question

Given a functor from a small category to $Set$, we can describe the colimit set as a quotient of the disjoint union of image sets by an equivalence relation arising from morphisms in the source category (as seen in Wikipedia, or Kashiwara-Schapira's Categories and Sheaves). I am looking for an analogous description on the 2-categorical level:

Is there an explicit description of "the" pseudo-colimit of a pseudo-functor $F$ from a small 2-category to $Cat$, and is it in the literature? In particular, who should I reference for the fact that such pseudo-colimits exist?

Here, by pseudo-colimit, I mean "pseudo-bi-colimit" in the sense of Borceaux's Handbook of Categorical Algebra, i.e., a pair $(L, \pi)$, where $L$ is a small category, and $\pi: F \to \Delta(L)$ is a pseudo-natural transformation to the constant pseudo-functor, such that the functor $Fun(L,B) \to PsNat(F, \Delta(B))$ given by $f \mapsto \Delta(f) \odot \pi$ is an equivalence.

Presumably, this should be a small category whose set of objects is something like a quotient of a disjoint union of object sets, but when I tried to work it out by myself, all of the arrows gave me a headache. I also looked at several sources, e.g., Kelly's Elementary Observations on 2-categorical limits, the elephant, and Borceaux, without success (but I may have missed something).

Answer 1

An answer can more or less be extracted from Kelly's Elementary Observations on 2-categorical limits, at least if you already know that it's there. (-:

First, as Kelly notes in section 6, it would suffice to construct what we may call strict pseudo-colimits, that is pseudo-colimits in your sense for which the functor $f\mapsto \Delta(f)\odot \pi$ is an isomorphism (since any isomorphism of categories is a fortiori also an equivalence).

Second, in Proposition 5.1, Kelly shows how to construct strict pseudo-limits (which he calls merely "pseudo-limits") in any 2-category out of (strict) products, cotensor products, iso-inserters, and iso-equifiers. This is a 2-categorical version of the construction of limits out of products and equalizers. (In the correction to the paper Fibrations in bicategories, Street gives an equivalent construction of non-strict pseudo-limits in terms of products, cotensor products, and descent objects.)

Dually, of course, pseudo-colimits may of course be constructed from coproducts, tensor products, iso-coinserters, and iso-coequifiers. Coproducts and tensor products in $Cat$ are easy — they are disjoint unions and cartesian products — so it suffices to construct iso-coinserters and iso-coequifiers.

At this level, though, I think we do have to descend into writing down strings of composites of arrows modulo equivalence relations. Iso-coinserters and iso-coequifiers, being both particular Cat-weighted colimits, can be constructed in terms of cartesian products in Cat and ordinary unweighted colimits, so it would suffice to understand the latter. We know that Cat is cocomplete (as a 1-category) since it is the models of an essentially algebraic theory, so this settles the existence question. But an explicit description of colimits is going to be kind of messy.

Answer 2

Here is my comment, rewritten as requested as an (elliptical) answer:

If you are content to consider diagrams indexed by 1-categories, you can find a simple construction in SGA 4 Expos\'e VI Section 6: it is the Grothendieck construction, associating a fibration to F (your "disjoint union"), followed by formal inversion of Cartesian morphisms in the fibration (your "quotient"). One thorough treatment of the general case (even with weights) is in Thomas Fiore's "Pseudo limits, biadjoints, and pseudo algebras."