The first and second corollary below are well-known category theory lemmas. We give a slightly different argument than usual (i.e. we took a trivial result and changed it into something much more complicated).

Here is a lovely little definition:

**Definition.** Given a small diagram of sets, write for the small category with

and morphisms

for and (where ), with composition induced by composition of maps .

**Example 1.** If , then a diagram is a pair of sets with parallel arrows . Then looks like a ‘bipartite preorder’ where every source object has outgoing valence :

**Example 2. **Given a set , write for the discrete category on , i.e. and

If is itself a discrete category, then is just a collection of sets, and

**Remark.** Giving a functor is the same thing as giving functors and natural transformations

of functors for all in , such that

for all in (where denotes horizontal composition of natural transformations, as in Tag 003G).

**Example 3.** Let be a small category, and consider the diagram given by the source and target maps . Then we have a functor

given on objects by

and on morphisms by

In terms of the remark above, it is given by the functors taking to and the natural inclusion , along with the natural transformations

We can now formulate the main result.

**Lemma.** *Let be a small category. hen the functor of Example 3 **is cofinal.*

Recall that a functor is *cofinal* if for all , the comma category is nonemptry and connected. See also Tag 04E6 for a concrete translation of this definition.

*Proof.* Let . Since , the identity gives the object in , showing nonemptyness. For connectedness, it suffices to connect any (i.e. ) to the identity ) (i.e. ). If , then the commutative diagram

gives a zigzag

of morphisms in connecting to . If instead , we can skip the first step, and the diagram

gives a zigzag

connecting to .

**Corollary 1.** *Let be a small diagram in a category with small products. Then there is a canonical isomorphism*

*provided that either side exists.*

*Proof.* By the lemma, the functor

is initial. Hence by Tag 002R, the natural morphism

is an isomorphism if either side exists. But is a category as in Example 1, and it’s easy to see that the limit over a diagram is computed as the equaliser of a pair of arrows between the products.

Of course this is not an improvement of the traditional proof, because the “it’s easy to see” step at the end is very close to the same statement as the corollary in the special case where is of the form for some . But it’s fun to move the argument almost entirely away from limits and into the index category.

**Corollary 2.** *Let be a category that has small products and equalisers of parallel pairs of arrows. Then is (small) complete. *