I am interested in the category-theoretic description of trees (and operads?) and have started a course of study that will allow me to engage with these two ([1](https://arxiv.org/pdf/0807.2874.pdf), [2](http://mat.uab.cat/%7Ekock/cat/polynomial.pdf)) manuscripts of Joachim Kock.


An essential prerequisite to the early portions of the manuscript involves an understanding of a pair of adjoint functors. The left adjoint is the change of basis functor $g^{\ast}: \mathbf{Set}\_{/A} \rightarrow \mathbf{Set}\_{/B}$ associated with the change of basis between sets $g: B \rightarrow A$. I find it very easy to reason about the image of a bundle under the change of basis functor. This functor takes a bundle $f: X \rightarrow A$ to the pullback of $f$ by $g$, which I can easily interpret in $\mathbf{Set}\_{/B}$ as the fibered product with the canonical projection $h: X \times\_{A} B \rightarrow B$ given by $h: (x, b) \mapsto b$.


Kock utilizes the right adjoint, which I have read is called the dependent product:
$$
 (g^\* \dashv \prod\_g)
 \colon
 \mathbf{Set}\_{/B}
 \stackrel{\overset{g^\* }{\leftarrow}}{\underset{\prod\_g}{\to}}
 \mathbf{Set}\_{/A}
 \,.
$$


I am trying to understand this functor, but am finding it very difficult. Are there any set-theoretic descriptions of the image of a bundle $f: X \rightarrow B$ under $\prod\_g$ that would help me in this context?


Although I've only had a little exposure to it, the process of re-describing adjoint functors in the "internal language of their categories" (I hesitate to use this phrase here-- I have seen it used in the literature of toposes and do not know its formal definition-- perhaps I'll just call this process *reifying*?) has proven very difficult for me. Are there any mental algorithms that offer any help? Are there a set of useful exercises I can undertake to develop the skill? Are there theorems I can study that will provide insight into the process?


It has struck me in the course of mulling over the problem that I would also like to know whether category-theorists even bother with reifying their constructions. Does this process have a name? Is it done often?



How do we describe the right adjoint?
It's worth thinking about the simplest example, namely when $A$ is a single point. In this case, $g^\*$ is the product functor $-\times B$, and its right adjoint is the set of sections: it sends $f\colon X\to B$ to the set $\Gamma(B,X)$ of sections $s\colon B\to X$ of $f$. This is vaguely similar behaviour to how the internal hom in a cartesian closed category is right adjoint to taking a product. In particular, if $X = Y\times B = g^\*Y$, then $\Pi\_g f = Y^B$.


The space of sections is the same thing as the product of all the fibres of $f$, so one can think of the general dependent product this way, now just parameterised by the elements of $A$. Given a point $a\colon \*\to A$, which is an object of $\mathbf{Set}/A$, we can calculate
$$
\mathbf{Set}/A(a,\Pi\_g f) \simeq \mathbf{Set}/B(B\times\_A \*,f) = \mathbf{Set}/B(g^{-1}(a),f)
$$
Now the latter is the set $\Gamma(g^{-1}(a),X)$ of sections of $f$ over $g^{-1}(a)\subset B$. But $\mathbf{Set}/A(a,\Pi\_g f)$ is the fibre of $\Pi\_g f \to A$ over $a$, so
$$
\Pi\_g f = \coprod\_{a\in A} \Gamma(g^{-1}(a),X) \to A.
$$


A similar mental picture works, to some extent, in categories that behave like the category of sets, except that you shouldn't think of $\Pi\_g f$ as a disjoint union, but something more like a continuous family of spaces of sections. Note howoever, how I used the defining property that it was a right adjoint to get a handle on the construction. In general, one can use [generalised elements](https://ncatlab.org/nlab/show/generalized+element) in place of $1\to A$ to construct the thing, at least as a presheaf, and then knowing the dependent product exists means this is representable.


