Return to Revisions

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 \to (\Gamma, x {:} A)$ 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$.