# Specifying morphisms of slice categories fibrewise.

I've been trying to figure out proposition 2.8 of Gambino and Kock 1.

The precise statemnet is (probably) not imporant but the context a locally cartesian closed category $\mathbf C$ where they are constructing an $A$-morphism $w : B \to B'$ in a slice $\mathbf C / A$. The statement confusing me is the following

... Since w must be an A-map, we can construct it fiberwise, so
we need for each a in A a map B'_a -> B_a. This allows
reduction to the case A = 1, ...


I'm unfamiliar with the notion of constructing such morphisms (in LCCCs other than Set) fibrewise. To me it seems they suggest that in order to specify a morphisms in $\mathbf C / A$ it is enough to specify all its images through the pullback functors along global elements (i.e. morphisms $1 \to A$), though I can't quite understand how I could have missed this.

Though my guess is that I am either being stupid and missing something utterly obvious or that I am to ignorant about reasoning using internal languages, I'm wondering if such morphisms can be defined by specifying their fibres (i.e. images of pullbacks along global elements).

Eagerly awaiting facepalm :)

-

It is not literally true that we can reduce to the case $A = 1$. For example, let $\mathcal{C}$ be the topos of sheaves on a non-trivial topological space, and let $A$ be any non-empty open set that isn't the whole space – then there is no morphism $1 \to A$ at all! Rather, what is true is that any slice of a locally cartesian closed category is again a locally cartesian closed category, and perhaps that is what they mean by reduction to the case $A = 1$. Or maybe they mean an argument using generalised elements – in which case the ordinary category-theoretic statement follows by taking the generalised element $a = \textrm{id}_A : A \to A$.
However, sometimes something more sophisticated can be said. Suppose $\mathcal{C}$ is a locally cartesian closed category with finite disjoint coproducts and coequalisers (e.g. any elementary topos), then the codomain fibration $\textrm{codom} : [\mathbb{2}, \mathcal{C}] \to \mathcal{C}$ is a stack for the extensive coverage on $\mathcal{C}$. This means it is literally true a morphism in the slice category $(\mathcal{C} \downarrow A)$ can be specified by a compatible family of morphisms in $(\mathcal{C} \downarrow U_1) \times \cdots \times (\mathcal{C} \downarrow U_n)$, where $U_1, \ldots, U_n$ constitute a covering family for $A$.
Let me explain what this means in the case of a regular epimorphism $\alpha : U \twoheadrightarrow A$. Form the kernel pair of $\alpha$, so that we have a coequaliser diagram: $$U \times_A U \rightrightarrows U \rightarrow A$$ Now, consider the triple adjunction induced by $\alpha : U \to A$ on slice categories: $$\Sigma_\alpha \dashv \alpha^* \dashv \Pi_\alpha : (\mathcal{C} \downarrow U) \to (\mathcal{C} \downarrow A)$$ This exists because $\mathcal{C}$ is locally cartesian closed. As usual, we get an induced monad $\mathbb{T} = (\alpha^* \Sigma_\alpha, \eta, \mu)$. Let $\epsilon : \Sigma_\alpha \alpha^* \Rightarrow \textrm{id}$ be the counit of the adjunction $\Sigma_\alpha \dashv \alpha^*$, and consider the diagram $$\Sigma_\alpha \alpha^* \Sigma_\alpha \alpha^* X \underset{\epsilon_{\Sigma_\alpha \alpha^* X}}{\overset{\Sigma_\alpha \alpha^* \epsilon_X}{\rightrightarrows}} \Sigma_\alpha \alpha^* X \overset{\epsilon_X}{\rightarrow} X$$ for each object $p : X \to A$ in $(\mathcal{C} \downarrow A)$. The pullback pasting lemma implies that this diagram is just $$U \times_A U \times_A X \underset{\pi_{2,3}}{\overset{\pi_{1,3}}{\rightrightarrows}} U \times_A X \overset{\pi_2}{\rightarrow} X$$ which is a coequaliser because $p^* : (\mathcal{C} \downarrow A) \to (\mathcal{C} \downarrow X)$ preserves all colimits. Thus $\alpha^*$ is a right adjoint of descent type. In particular, to specify a morphism $f : X \to Y$ in $(\mathcal{C} \downarrow A)$, it is enough to specify a morphism $\tilde{f} : U \times_A X \to U \times_A Y$ in $(\mathcal{C} \downarrow U)$ making the diagram $$\begin{array}{ccc} U \times_A U \times_A X & \overset{\pi_{1,3}}{\longrightarrow} & U \times_A X \\ {\scriptsize U \times_A \tilde{f}} {\Large \downarrow} & & {\Large \downarrow} {\scriptsize \tilde{f}} \\ U \times_A U \times_A Y & \underset{\pi_{1,3}}{\longrightarrow} & U \times_A Y \end{array}$$ commute. (Strictly speaking, this is monadic descent, but this is equivalent to descent for fibred categories in the case of the codomain fibration by e.g. the Bénabou–Roubaud theorem.)