The morphism $f$ is invisible in type theory because it corresponds to weakening, which type theory exhibits schematically. More precisely, given a context $\Gamma$ and a type family $\Gamma \vdash A \; \mathsf{type}$
there is a substitution $\iota : (\Gamma, x {:} A) \to \Gamma$ which takes each variable $y \in \Gamma$ to itself (but is not identity, it's shifting in terms of de Bruijn indices). This is your $f$. It induces a weakening operation $\iota^{*} : \mathsf{Type}(\Gamma) \to \mathsf{Type}(\Gamma, x{:}A)$ that takes a type family over $\Gamma$ to a type family over $\Gamma, x {:} A$. The dependent product and sum go in the opposite direction
$$\Pi, \Sigma : \mathsf{Type}(\Gamma, x{:}A) \to \mathsf{Type}(\Gamma)$$
and their rules state precisely that there are adjunctions $\Sigma \vdash \iota^{*} \vdash \Pi$.