# Checking the functoriality of an expression involving dependent sum and product

I'm unsure if my question is advanced enough for this site, but let's see.

Let $$\mathcal{C}$$ be a locally cartesian closed category, so that it always has dependent products $$\Pi_f$$, i.e., right adjoints to base change functors $$f^{\ast}$$, along with dependent sums $$\Sigma_f$$, i.e., left adjoints to base change functors. In the article Simplicial Model of Univ. Foundations, Definition 1.4.1 is an expression $$U^{\sqcap}\equiv \underbrace{\Sigma_{U \rightarrow 1}}_{F(U)} \underbrace{\Pi_{\tilde{U} \rightarrow U}}_{G(U)}\left(\underbrace{\pi_{2}: U \times \tilde{U} \rightarrow \tilde{U}}_{H(U)}\right)$$ where $$\tilde{U}\to U$$ refers to a particular morphism $$p$$ with which $$U$$ comes equipped. (This morphism gives the structure of a so-called universe in $$\mathcal{C}$$, but this shouldn't be essential to my question.)

Now, the authors refer to the "evident functoriality" of $$U^{\sqcap}$$ in $$U$$. But I just don't see this.

$$U^{\sqcap}$$ has the form $$F(U)(G(U)(H(U)))$$ where $$F$$ and $$G$$ refer to functors defined in terms of $$U$$ and $$H$$ is a functor on pairs of objects in $$\mathcal{C}$$. If we are given a morphism $$(f,g)$$ in the arrow category of $$\mathcal{C}$$ from $$\tilde{U}'\to U'$$ to $$\tilde{U}\to U$$, we get an induced map $$H(f,g):\pi_2' \to \pi_2$$. I also believe that we can view $$\Pi_{-}$$ and $$\Sigma_{-}$$ as functors from the arrow category of $$\mathcal{C}$$ to the arrow category of $$\text{CAT}$$. But I'm getting nowhere with trying put this all together to find an induced map $$(f,h)^{\sqcap}:\left(U'\right)^{\sqcap} \to U^{\sqcap}$$.

I'm likely missing something obvious, but any help would be much appreciated.

You are right that $$(-)^{\mathsf \Pi}$$ is not functorial on the arrow category of $$\mathcal{C}$$. However, it is functorial on the category whose objects are arrows in $$\mathcal{C}$$ and whose morphisms are pullback squares, and I believe that's what the authors were referring to, since in their case $$\tilde{U_0}$$ is defined as the pullback of $$\tilde{U}$$ to $$U_0$$.
Given a pullback square $$\require{AMScd}$$ $$\begin{CD} \tilde{U}' @>f>> \tilde{U} \\ @V p' VV @VV p V \\ U' @>>g> U \end{CD}$$ we have a map $$\tilde{U}' \times U' \to \tilde{U} \times U$$ over $$f$$ and hence a map $$\tilde{U}' \times U' \to f^*(\tilde{U} \times U)$$ over $$\tilde{U}'$$, thus by functoriality a map $$(U')^{\mathsf{\Pi}} = \Pi_{p'}(\tilde{U}'\times U') \to \Pi_{p'}(f^*(\tilde{U}\times U))$$. But by the Beck-Chevalley condition for the pullback square we have $$\Pi_{p'}(f^*(\tilde{U}\times U)) \cong g^*(\Pi_p(\tilde{U}\times U)) = g^*(U^{\mathsf{\Pi}})$$, so we get a map $$(U')^{\mathsf{\Pi}} \to g^*(U^{\mathsf{\Pi}})$$ over $$U'$$, hence a map $$(U')^{\mathsf{\Pi}} \to U^{\mathsf{\Pi}}$$ over $$g$$.