Dependent products are said to be the right adjoints of reindexing functors according to nlab. However, I can only make sense of this explanation in the context of type theory, where dependent products correspond to the dependent product type (the pi type).
Since dependent products have a pure category-theoretical definition, is there demonstrations of dependent products that are useful in non-type-theory contexts?
Dependent products appear explicitly in many places in mathematics, long predating category theory and type theory. The terminology they most often appear under is “the product of a family of sets” (or set-based objects); also quite often they are described as the set of “functions/operations assigning to each (something) a (something dependent on it)”.
For instance, picking up the first textbooks I see that are absolutely not dependent on type theory or category theory:
Atiyah and Macdonald Commutative Algebra defines (Ch.II, p.20) the direct product of an arbitrary family of modules, $\prod_{i \in I} M_i$.
Jech Set Theory (3rd Millennium edition) defines (p.53, 5.14) the product of an arbitrary family of sets $\prod_{i \in I} X_i$, to exhibit the axiom of choice as “the product of a family of non-empty sets is non-empty”.
Other answers give many important specific examples — but the point I want to illustrate is that the general construction was already very traditional and widespread.
Dependent products exist in set theory, and are used routinely in this setting. The trick is that they are typically used without mentioning that they are indeed dependent products. Two examples that come to my mind:
A very elementary example is the rule for multiplying out brackets:
$$\prod_{i\in I}\sum_{j\in J_i}x_{ij}=\sum_{f\in\prod_iJ_i}\prod_{i\in I}x_{if(i)}$$
where the dependent product appears in the subscript of the sum on the right hand side.
I'm really interested in a good explanation too but I'll give my little bit.
I prefer thinking in terms of spans rather than slice categories. Recall composition of spans is basically dependent sum.
The adjoint/residual of spans is basically the same as Kan extension for profunctors but is also dependent producty.
$$ (P/Q)(A, B) = \forall C, P(C, A) \rightarrow Q(C, B) $$
Profunctors can also be seen as a sort of span as two sided discrete fibrations.
I like the view of spans as double categories best.
I would then see dependent product as the adjoint to composition of horizontal maps in a double category.
Not sure this is a good place for the question but not sure of a better one exactly.
In formal semantics of natural languages we do have examples too:
https://ncatlab.org/nlab/show/dependent+type+theoretic+methods+in+natural+language+semantics
I was unsure about giving another answer because this is sort of shaky.
You know how I mentioned adjoints to composition (which is basically pullback) are dependent producty?
A concrete example I ran into recently is the category of relations $\text{Rel}$.
Composition of two relations is a form of existential quantification $(P \circ Q)(a, b) = \exists x. P(a, x) \wedge Q(x, b)$ and in a definite style corresponds to equality in first order logic. An adjoint here ought to correspond to Hilbert's epsilon operator which is a fancy but problematic way of defining existential quantification.
I'm still shaky about Hilbert's epsilon calculus but you ought to have a relationship along the lines of
$$ \frac{P(E)}{(\varepsilon x\colon A. P(x)) = E} $$
You can see this as similar to the $\mu$ and $\tilde{\mu}$ operators in $\bar{\lambda} \mu \tilde{\mu}$ calculus (which corresponds to System LK.) The calculus has similar rules for composition (cut.) I'm not sure I recall things precisely but you want rules like
$$ \langle \mu x. c(x) \mid E \rangle \longrightarrow c(E) $$
$$ \langle v \mid \tilde{\mu} x. c(x) \rangle \longrightarrow c(v) $$
Unfortunately $\langle \mu x. c(x) \mid \tilde{\mu} x. c(x) \rangle$ is ambiguous and you have to fix an evaluation order and this is problematic in a dependently type setting. Hilbert's epsilon has similar weird issues. There are workarounds but they probably involve heavyweight stuff like linear logic.
It's surprising the adjoint to composition turns up in both a continuations based control flow construct and in the indefinite description operator.
Except while Kan extension for relations is dependent producty $\forall x. P(x, a) \rightarrow Q(x, b)$ Kan extension for regular old functors is shaped like the continuation monad $\forall x. (A \rightarrow F(x)) \rightarrow G(x)$!
