For a category $\mathbf C$, the category of families of $\mathbf C$, denoted $\mathrm{Fam}(\mathbf C)$ is the free coproduct completion of $\mathbf C$. Explicitly, the objects of $\mathbf C$ are given by set-indexed families $(A_i)_{i \in I}$ of objects of $\mathbf C$, and morphisms $(A_i)_{i \in I} \to (B_j)_{j \in J}$ are given by functions $f : I \to J$ together with families of morphisms $(f_i : A_i \to B_{f(i)})_{i \in I}$.
The $\mathrm{Fam}$-construction is well known in category theory. However, it is difficult to track down the original reference, as it appears to have been well known for a long time, and is often introduced without citing an earlier text. I would like to know where this construction and its universal property first appears in print (or elsewhere).
The two earliest references I have found so far are:
- Diers's Catégories localisables (1977), where the notation $\mathbb F(\mathbf C)$ is used; the universal property does not appear to be given there.
- Bénabou's Fibered Categories and the Foundations of Naive Category Theory (1985), where the notation $\mathrm{Fam}(\mathbf C)$ appears and its universal property is given.
Considering that the same name for the construction is given in both papers, but Bénabou does not cite Diers, it seems plausible that there is an earlier reference for the construction and it was already well-known in 1985. I would be happy to receive information otherwise (though I appreciate is it difficult to prove there is not an earlier reference).