For example, $\forall x \in X, P(x)$ can be viewed as a map $P : X \to \text{TrueProp}$ the collection of true propositions.
Why do we make the distinction in type theory, which seems to want to reduce all constructions down to a few building blocks? In type theory $\forall$ is a handled using what's called a Pi-type, usually, but why didn't they just handle it using a mapping of types?
Certain $\forall$ statements become even more obviously just a map, as in $\forall x \in X, f(x) \in Y$ is the same thing as $f: X \to Y$.
I'm experimenting with software implementations of logic / math, so that's why I've asked this.
I'm going to assume we're talking about a standard type theory, something that's only a minor variation on the lambda cube systems. This said, the two things differ in several important ways.
For one, the $f$ in $f:A\to \mathsf{Prop}$ is not a thing which can have terms of its own; $x:f$ makes no sense in the language. On the other hand, the whole point of $\Pi(x:A).B(x)$ is it's a type which can have terms.
The term $f$ also does something entirely different from a term $g:\Pi(x:A).B(x)$. If $a:A$, then $f(a)$ is a term of type $\mathsf{Prop}$. On the other hand, $g(a)$ is a term of type $B(a)$, not $\mathsf{Prop}$. This is really the central purpose of Pi-types. There are no inference rules that let you take $f$ and generate a term of type $f(a)$ when given an $a:A$. Certainly, if we have a proof of $\forall (x:A).B(x)$, we should expect to be able to derive a proof of each instance $B(a)$, and this is something you can't do with just a map $B:A\to\mathsf{Prop}$.