I'll expand on Simon Henry's comment to a full answer.
We first define the disjunction of two types. Recall that traditionally, the disjunction of $A$ and $B$ is defined as the propositional truncation of the coproduct of $A$ and $B$:
$$A \vee B \equiv [A + B].$$
Using the impredicative definition of propositional truncation above, we then have
$$A \vee B \equiv \prod_{P:\mathrm{Prop}} ((A + B) \to P) \to P.$$
For all types $A$, $B$, and $C$, there is an equivalence
$$((A + B) \to C) \simeq ((A \to C) \times (B \to C))$$
and if $A \simeq B$, then $(A \to C) \simeq (B \to C)$. In addition, for all type families $x:A \vdash B(x)$, and $x:A \vdash C(x)$, if there is a family of equivalences $e:\prod_{x:A} B(x) \simeq C(x)$, then there is an equivalence $\left(\prod_{x:A} B(x)\right) \simeq \left(\prod_{x:A} C(x)\right)$. All this taken together means that there is an equivalence
$$\left(\prod_{P:\mathrm{Prop}} ((A + B) \to P) \to P\right) \simeq \left(\prod_{P:\mathrm{Prop}} ((A \to P) \times (B \to P)) \to P\right).$$
Uncurrying $((A \to P) \times (B \to P)) \to P$ in the above expression leads to Simon Henry's equivalent definition of the disjunction of two types.
$$A \vee B \equiv \prod_{P:\mathrm{Prop}} (A \to P) \to (B \to P) \to P$$
From there it is easy to define the booleans as the type
$$\mathrm{bool} \equiv \sum_{P:\mathrm{Prop}} P \vee \neg P$$
and the coproduct types as
$$A + B \equiv \sum_{x:\mathrm{bool}} C(x)$$
where $C(\bot) \equiv A$ and $C(\top) \equiv B$.
On a side note, the same logic could be used to define the existential quantifier without using dependent sum types. We have the equivalence
$$\left(\prod_{P:\mathrm{Prop}} \left(\left(\sum_{x:A} B(x)\right) \to P\right) \to P\right) \simeq \left(\prod_{P:\mathrm{Prop}} \left(\prod_{x:A} B(x) \to P\right) \to P\right).$$
Thus, we could define
$$\exists x:A.B(x) \equiv \prod_{P:\mathrm{Prop}} \left(\prod_{x:A} B(x) \to P\right) \to P.$$
In a similar way, we can also define the empty type from the type of propositions. The empty type is a proposition, and thus is equivalent to its propositional truncation. By recursion on the empty type, every function type from the empty type is contractible and equivalent to the unit type. Now, every function type from a contractible type is equivalent to the codomain of the function type; thus, we have the following equivalences
$$\emptyset \simeq \left(\prod_{P:\mathrm{Prop}} (\emptyset \to P) \to P\right) \simeq \left(\prod_{P:\mathrm{Prop}} \mathbb{1} \to P\right) \simeq \prod_{P:\mathrm{Prop}} P$$
and we could define
$$\emptyset \equiv \prod_{P:\mathrm{Prop}} P.$$
The resulting empty type is $U$-large.
The key thing here is that since each $P$ is a prop, by weak function extensionality, the type $\prod_{P:\mathrm{Prop}} P$ is also a proposition. If the type $\prod_{P:\mathrm{Prop}} P$ has an element, then every proposition has an element and is thus contractible, which implies that the universe $U$ itself is contractible and thus trivial. But we do not know if $\prod_{P:\mathrm{Prop}} P$ has an element, so $\prod_{P:\mathrm{Prop}} P$ behaves as the empty type.
Best Answer
The morphism $f$ is invisible in type theory because it corresponds to weakening, which in type theory appears as context extension, rather than an explicitly applied substitution.
Type-theoretic explanation
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$.
Set-theoretic explanation
Let us also explain what $\iota$ corresponds to set-theoretically. There are two equivalent ways of giving a set-theoretic interpretation, namely families and display maps. You indicated in your question that you prefer the latter, so let us use that. (The families are more natural, please consult Section 5.1 of my notes on realizability for details.)
A context is a set. The empty context is the singleton set.
A type family $\Gamma \vdash A \; \mathsf{type}$ is an element of the slice $\mathsf{Set}/\Gamma$, which we write as $p_A : \overline{A} \to \Gamma$.
A term of type $A$ in context $\Gamma$ is a section $t : \Gamma \to \overline{A}$ of $p_A$, i.e., it has to satisfy $p_A \circ t = \mathsf{id}$. In particular, this means that from $t(\gamma) \in \overline{A}$ we can reconstruct $\gamma = p_A(t(\gamma))$, which means that $t(\gamma)$ should not be thought of as "one element of $A$", but rather as "one element of $A$ together with an environment $\gamma$".
Given a type family $p_A : \overline{A} \to \Gamma$, the context extension $\Gamma, x {:} A$ is the set $\overline{A}$.
A substitution is a map $\sigma : \Gamma \to \Delta$. Specifically, the above substitution $\iota : (\Gamma, x {:} A) \to \Gamma$ is just the map $p_A : \overline{A} \to \Gamma$.
The action of $\sigma : \Gamma \to \Delta$ is pullback $$\sigma^* : \mathsf{Set}/\Delta \to \mathsf{Set}/\Gamma.$$ When we plug in $p_A$ we get the pullback $$p_A* : \mathsf{Set}/\Gamma \to \mathsf{Set}/\overline{A}.$$ It has left and right adjoints $\Sigma_A \dashv p_A^* \dashv \Pi_A$. I can spell them out if you wish.