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](https://arxiv.org/pdf/1211.2851.pdf), 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.



Checking the functoriality of an expression involving dependent sum and product
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$.


