# Can function types be represented using $\Sigma$-types

logictype-theory

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?

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$$