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.