Post History

Generalization of categorical product

I'm only a dabbler in category theory; this might be a basic concept just outside of my sphere of exposure.

I'm looking for references to the following universal construction, a generalization of the categorical product.

Given a category $\mathcal{C}$ and a functor $F$ from $\mathcal{C}$ to some other category, for any two objects $X_1, X_2$ of $\mathcal{C}$, the ‘$F$-product’ $X_1 \times_F X_2$, if it exists, is an object of $\mathcal{C}$ equipped with two morphisms $\pi_i : X_1 \times_F X_2 \to X_i$ such that:
 * each $F(\pi_i)$ is an identity morphism
 * for any two morphisms $f_i : Y \to X_i$ where $F(f_1) = F(f_2)$, there exists a unique $f : Y \to X_1 \times_F X_2$ with $\pi_i \circ f = f_i$

We recover the usual categorical product if $F$ is any constant functor. (Or at least, that's my intent; if not I've probably misstated something.) For more interesting functors, $F$-products may exist where usual products don't, because the component morphisms are constrained to agree under $F$.

I haven't found anything called an ‘$F$-product’ yet but of course the canonical name for this thing, if it exists, is not required to be that unimaginative.

Any pointers?