How do dependent products in category theory relate to type theory? I feel like I understand the construction of dependent product types relatively well, it makes sense to me how the introduction and elimination rules work together to create the concept of a function whose co-domain depends on the values of the function in the domain, but given the definitions and motivation on n-cat lab for the corresponding notion in category theory, I don't get the same intuition.
Given an element $x : I \rightarrow A$ in a category, and a categorical dependent product $f = \Pi_{x : A} F(x) $, it isn't even clear to me how one would obtain the element $f(x) : F(x)$, like one can using the elimination rule of the dependent product in type theory. More generally, I'd like to see a more explicit connection with the dependent product in type theory.
 A: Uff.  It's hard to talk about this without introducing all of categorical type theory.  The general notion is the notion of a comprehension category which I believe was introduced by Bart Jacobs.  See his book or his thesis.  However, when I did a search to get a reference for some definitions I found this recent set of notes, "Type Theory through Comprehension
Categories" by Paolo Capriotti, which is pretty good.
We start with a category $\mathcal{C}$ whose objects we're going to think of as contexts which we'll think of as roughly lists of types.  Given this, the type $\tau$ in context $\Gamma$ will be represented by an arrow $p_\tau : \Gamma,\tau\longrightarrow\Gamma$ called a display map which will be used to represent weakening.  (Usually, only a subset of arrows will be designated as display maps.)  We might notate a type-in-context as $\Gamma \vdash \tau$.  So a type over $\Gamma$ is an object of the slice category $\mathcal{C}/\Gamma$.  A term, $M$, of type $\tau$ is an arrow $M : \Gamma\longrightarrow\Gamma,\tau$ such that $p_\tau \circ M = id$.  Typically this would be notated as $\Gamma \vdash M : \tau$.  In other words, $M$ is an arrow from $id_\Gamma \to p_\tau$ in $\mathcal{C}/\Gamma$.  An arbitrary arrow in $\mathcal{C}$, $\sigma : \Delta\longrightarrow\Gamma$ represents a substitution.  Intuitively, it's a substitution for variables in $\Gamma$ in terms of variables in $\Delta$.  These arrows give rise to functors $\sigma^* : \mathcal{C}/\Gamma\longrightarrow \mathcal{C}/\Delta$.  To interpret $\sigma^*$ we require $\mathcal{C}$ to have pullbacks.
$$\require{AMScd}
\begin{CD}
\Delta,\tau[\sigma] @>>> \Gamma,\tau \\
@V\sigma^*(p_\tau)VV @VVp_\tau V \\
\Delta @>>\sigma> \Gamma
\end{CD}$$
The action of $\sigma^*$ on arrows, i.e. terms, we might notate as $\Delta \vdash M[\sigma] : \tau[\sigma]$.  The operation $(-)^*$ is itself pseudofunctorial meaning it preserves composition and identities only up to isomorphism.  (This pseudofunctoriality, while a little to rigid to be completely natural categorically [it corresponds to a cloven fibration], is too loose type theoretically where, because we have syntax, we expect everything to hold "on the nose".  Getting strict functoriality precipitates a lot of the complexity in this field.)
With that in place, the dependent product for a type $\tau$ is the right adjoint of $p_\tau^*$.  $p_\tau^* \dashv \Pi_\tau : \mathcal{C}/\Gamma,\tau \to \mathcal{C}/\Gamma$.  (Obviously we are going to want the adjoint to exist for all types and for them to fit together appropriately.  The coherence conditions are called the Beck-Chevalley conditions.)  We can write the action of $\Pi_\tau$ on a type as $$\frac{\Gamma,x:\tau\vdash B}{\Gamma\vdash\Pi x:\tau.B}$$ In particular we have the natural isomorphism $$\mathcal{C}/\Gamma,A(p_A^*(-),=) \cong \mathcal{C}/\Gamma(-, \Pi_A(=))$$
which if we instantiate to $id_\Gamma$ and $p_B$ gives a mapping on arrows (essentially terms) that in type theoretic notation would look like
$$\frac{\Gamma,x:A\vdash M:B}{\Gamma\vdash\lambda x\!:\!A.M : \Pi x\!:\!A.B}$$
and post-composition by the counit gives a natural transformation of hom-functors
$$\mathcal{C}/\Gamma,A(-,p_A^*(\Pi_A(=))) \to \mathcal{C}/\Gamma,A(-,=)$$
which, instantiating with $id_{\Gamma,A}$ and $p_B$, gives
$$\frac{\Gamma,x:A\vdash M:\Pi y\!:\!A.B}{\Gamma,x:A\vdash Mx : B[y\mapsto x]}\quad x \text{ not free in } B$$
This rule represents a commutative triangle to which we can apply the substitution functor induced by the (underyling arrow of the) term $\Gamma \vdash N : A$ to get the more usual
$$\frac{\Gamma\vdash N:A \quad \Gamma\vdash M:\Pi x\!:\!A.B}{\Gamma\vdash MN : B[x\mapsto N]}$$
(Actually this is slightly different from what I stated and more corresponds to doing $\sigma^*(\varepsilon_{p_B} \circ M[p_A^*])$ where $\sigma$ is the substitution induced by $N$.)
I've been fairly sloppy in this presentation, assuming certain properties hold strictly that may not.  See the links above for explications of those details and how to deal with them.
