[proofplan] The proof is an unpacking of the Beck-Chevalley hypotheses with all typing made explicit. First we form the pullback of the display map $\theta$ along the substitution $\phi$ and use closure of $\mathcal D$ under pullback to ensure that the substituted display map $\theta'$ is still one of the maps for which the chosen adjoints exist. Then the right-adjoint Beck-Chevalley isomorphism gives stability of $\Pi_\theta$ under substitution, and the left-adjoint Beck-Chevalley isomorphism gives stability of $\Sigma_\theta$ under substitution, possibly after inverting the chosen comparison depending on the convention for its orientation. The one-sided conclusions use only the corresponding one-sided Beck-Chevalley assumption. [/proofplan] [step:Pull back the display map along the substitution] Fix a display map $\theta:\Delta\to\Gamma$ in $\mathcal D$ and a context morphism $\phi:\Gamma'\to\Gamma$. Let $\Delta'$ be a chosen pullback of $\theta$ along $\phi$, and let \begin{align*} \theta':\Delta'\to\Gamma' \end{align*} and \begin{align*} \phi':\Delta'\to\Delta \end{align*} denote the induced morphisms, so that \begin{align*} \theta\circ\phi'=\phi\circ\theta'. \end{align*} Since $\mathcal D$ is closed under pullback along context morphisms and $\theta$ belongs to $\mathcal D$, the pulled-back morphism $\theta'$ also belongs to $\mathcal D$. Therefore the chosen adjoints associated to $\theta'$ exist: \begin{align*} \Sigma_{\theta'}\dashv(\theta')^*\dashv\Pi_{\theta'}. \end{align*} For any object $B\in\mathcal E_\Delta$, the reindexed object \begin{align*} (\phi')^*B\in\mathcal E_{\Delta'} \end{align*} is defined, and hence both $\Pi_{\theta'}((\phi')^*B)$ and $\Sigma_{\theta'}((\phi')^*B)$ are objects of $\mathcal E_{\Gamma'}$. [guided] We first identify the substituted context extension. The display map \begin{align*} \theta:\Delta\to\Gamma \end{align*} represents a type or context extension over $\Gamma$, while the morphism \begin{align*} \phi:\Gamma'\to\Gamma \end{align*} represents substitution from $\Gamma'$ into $\Gamma$. Pulling $\theta$ back along $\phi$ gives a context $\Delta'$ equipped with morphisms \begin{align*} \theta':\Delta'\to\Gamma' \end{align*} and \begin{align*} \phi':\Delta'\to\Delta \end{align*} satisfying \begin{align*} \theta\circ\phi'=\phi\circ\theta'. \end{align*} This equation is the categorical expression that $\Delta'$ is the substituted extended context. The hypothesis that $\mathcal D$ is closed under pullback is used at exactly this point: because $\theta$ is a display map in $\mathcal D$, its pullback $\theta'$ is again a display map in $\mathcal D$. Hence $\theta'$ is eligible for the chosen adjoint structure. Thus the adjunctions \begin{align*} \Sigma_{\theta'}\dashv(\theta')^*\dashv\Pi_{\theta'} \end{align*} exist. If $B\in\mathcal E_\Delta$ is a type family over $\Delta$, then substitution along $\phi'$ gives \begin{align*} (\phi')^*B\in\mathcal E_{\Delta'}. \end{align*} Applying the chosen dependent product and dependent sum functors along $\theta'$ then gives objects \begin{align*} \Pi_{\theta'}((\phi')^*B)\in\mathcal E_{\Gamma'} \end{align*} and \begin{align*} \Sigma_{\theta'}((\phi')^*B)\in\mathcal E_{\Gamma'}. \end{align*} These are the interpretations obtained by substituting into the family first and forming the dependent product or sum afterwards. [/guided] [/step] [step:Apply the right-adjoint Beck-Chevalley isomorphism to dependent products] Let $B\in\mathcal E_\Delta$. The object $\Pi_\theta B$ lies in $\mathcal E_\Gamma$, so substitution along $\phi$ gives \begin{align*} \phi^*(\Pi_\theta B)\in\mathcal E_{\Gamma'}. \end{align*} By the assumed Beck-Chevalley condition for the right adjoints in the pullback square determined by $\phi$ and $\theta$, the chosen comparison morphism is an isomorphism. With the orientation used in the statement, this gives an isomorphism in $\mathcal E_{\Gamma'}$ \begin{align*} \phi^*(\Pi_\theta B)\cong \Pi_{\theta'}((\phi')^*B). \end{align*} If the chosen convention defines the right-adjoint comparison in the opposite direction, we use its inverse, which exists because the Beck-Chevalley comparison is assumed to be an isomorphism. This is precisely substitution stability for dependent products: forming the dependent product along $\theta$ and then substituting along $\phi$ agrees, up to the specified Beck-Chevalley isomorphism, with first substituting $B$ along $\phi'$ and then forming the dependent product along $\theta'$. [/step] [step:Apply the left-adjoint Beck-Chevalley isomorphism to dependent sums] Again let $B\in\mathcal E_\Delta$. The object $\Sigma_\theta B$ lies in $\mathcal E_\Gamma$, so substitution along $\phi$ gives \begin{align*} \phi^*(\Sigma_\theta B)\in\mathcal E_{\Gamma'}. \end{align*} By the assumed Beck-Chevalley condition for the left adjoints in the same pullback square, the chosen comparison morphism is an isomorphism. If the comparison is chosen in the orientation \begin{align*} \Sigma_{\theta'}((\phi')^*B)\cong \phi^*(\Sigma_\theta B), \end{align*} then inverting that isomorphism gives \begin{align*} \phi^*(\Sigma_\theta B)\cong \Sigma_{\theta'}((\phi')^*B). \end{align*} If instead the comparison is chosen directly in the displayed orientation, no inversion is needed. Thus forming the dependent sum along $\theta$ and then substituting along $\phi$ agrees, up to the specified Beck-Chevalley isomorphism, with first substituting $B$ along $\phi'$ and then forming the dependent sum along $\theta'$. [/step] [step:Extract the one-sided variants from the same argument] The proof of the dependent-product isomorphism used only the existence of the right adjoints $\theta^*\dashv\Pi_\theta$ and the Beck-Chevalley isomorphisms for those right adjoints. Therefore, under the one-sided hypotheses for $\Pi$-types alone, the argument gives \begin{align*} \phi^*(\Pi_\theta B)\cong \Pi_{\theta'}((\phi')^*B). \end{align*} The proof of the dependent-sum isomorphism used only the existence of the left adjoints $\Sigma_\theta\dashv\theta^*$ and the Beck-Chevalley isomorphisms for those left adjoints. Therefore, under the one-sided hypotheses for $\Sigma$-types alone, the argument gives \begin{align*} \phi^*(\Sigma_\theta B)\cong \Sigma_{\theta'}((\phi')^*B). \end{align*} Combining the two one-sided arguments under the two-sided hypotheses proves the stated substitution stability for both dependent products and dependent sums. [/step]