Can function types be represented using $\Sigma$-types? Fix types $A, B : \mathsf{Type}$, and let $\mathbf{2} = \{ 0, 1 \} : \mathsf{Type}$ be a two-element type. We define

*

*$B' : A \to \mathsf{Type}$ by $B'(a) = B$.

*$C : \mathbf{2} \to \mathsf{Type}$ by $C(0) = A$, $C(1) = B$.

Using $\Pi$- and $\Sigma$-types, we can encode some of the basic propositional type formers:

*

*The function type $A \to B$ can be represented as $\prod_{(a:A)} B'(a)$.

*The sum type $A + B$ can be represented as $\sum_{(i:\mathbb{2})} C(i)$.

*The product type $A \times B$ can be represented in two different ways: either as $\sum_{(a:A)} B'(a)$ or as $\prod_{(i:\mathbb{2})} C(i)$.

So, we get something like the following table:
$$\begin{array}{c|cc}
       & (A, B')      & (\mathbb{2}, C) \\
\hline
\Pi    &  A \to B     &  A \times B     \\
\Sigma &  A \times B  &  A + B          \\
\end{array}$$
Question: is it possible to represent $A \to B$ as a $\Sigma$-type, or $A + B$ as a $\Pi$-type?
 A: If you allow quantification over $\mathsf{Type}$, then $A \times B$ and $A + B$ have the following definitions as $\Pi$-types:
$$
  A + B := \Pi_{(C: \mathsf{Type})} (A \to C) \to (B  \to C) \to C \\
  A \times B := \Pi_{(C: \mathsf{Type})} (A \to (B \to C)) \to C
$$
where every $\to$ could be further replaced by a $\Pi$-type, as you also illustrated.
When it comes to $A \to B$ as a $\Sigma$-type, then (apart for the case where $A$ is some finite type*) I am less convinced that it will work out. One thing to note is that $\Sigma$-types can also be defined in terms of $\Pi$-types. Given $P : A \to \mathsf{Type}$ we can define
$$
  \Sigma_{(a :A)} P(a) := 
  \Pi_{(C : \mathsf{Type})} ( \Pi_{(a : A)} (P(a) \to C)) \to C 
$$

$^*$ If we refer to $\mathsf{n}$ as the type with $n$ terms, then (depending on the exact meaning of $\equiv$) you could probably do something like:
$$
  \mathsf{(n+1)} \to B 
  \equiv \Pi_{(x \, : \, \mathsf{(n+1)})} B
  \equiv B \times \Pi_{(x \, : \, \mathsf{n})} B
  \equiv \Sigma_{(b : B)} \, \Pi_{(x \, : \, \mathsf{n})} B
  \equiv \Sigma_{(b : B)} \, (\mathsf{n} \to B)
$$
and then continue this until we reach $\mathsf{0} \to B \equiv \mathsf{1}$. This is really just trying to imitate exponentiation of a number $a : \mathbb{N}$ with some natrual number:
$$
 a^4 = a \cdot a^3 = \sum_{i = 1}^a a^3 = \sum_{i = 1}^a a \cdot a^2
 = \dots = \sum_{i = 1}^a \sum_{j = 1}^a\sum_{k = 1}^a\sum_{l = 1}^a 1
$$
