Formalizing constant symbols as terms in type theory. In type theory, we usually define each type with a constant symbol, e.g., the dependent product uses '$\Pi$', the dependent sum uses '$\Sigma$', the sum/coproduct uses '$+$'. I noticed that we could possibly reformulate these symbols as terms within the language itself. To demonstrate, we introduce a constant term '$\Pi$' such that given any type $A$ and any function $B$ from $A$ to types, $\Pi\ A\ B$ is also a type. Formally, let $x$ be a variable and $A$ and $B$ be terms;
$$\begin{array}{c}
A:\mathsf{Type}\quad x:A\vdash B\ x:\mathsf{Type} \\
\hline
\Pi\ A\ B:\mathsf{Type}
\end{array}$$
where $x$ does not occur free in $A$ nor $B$. Other types can be constructed similarly. For my question, is there any interesting consequences/benefits to formulizing a type theory this way, or is there any good reason it should not be done like this?
I thought it might be interesting since under this formulation, we can manipulate the $\Pi$ term itself, as well as abstract over its second argument, e.g.,
$$\lambda A:\mathsf{Type}\ .\lambda B:(\Pi\ A\ x:A\ .\mathsf{Type})\ .\Pi\ A\ B,$$
all of which I haven't seen done in traditional type theory. Additionally, $\Pi$ is typable:
$$\Pi:\Pi\ \mathsf{Type}\ A:\mathsf{Type}\ .\Pi\ (\Pi\ A\ x:A\ .\mathsf{Type})\ B:(\Pi\ A\ x:A\ .\mathsf{Type})\ .\mathsf{Type}.$$
 A: The issue here is in the very definition of the $\Pi$ type. The only type which must be a primitive is the $\Pi$ type - the rules for other types can be defined in terms of the rules for $\Pi$.
I will assume you're using infinite universes. Rather than $\mathsf{Type}$, I will write $\mathsf{Type}_i$ for the $i$th level of types.
Consider the judgement $A : \mathsf{Type}_0 \vdash \lambda x : A . \mathsf{Type}_j : \Pi A (\lambda x : A . \mathsf{Type}_{j + 1})$. I claim that this judgement can never be made.
For if we were to make this judgement using your rule, we would first need the judgement $A : \mathsf{Type}_0, x : A \vdash (\lambda x . \mathsf{Type}_j) x : \mathsf{Type}_{j + 1}$. And in order to come to this conclusion, we would need to apply the elimination rule, which states that
$$\begin{array}{c}
A:\mathsf{Type_i}\quad x:A\vdash B\ x:\mathsf{Type_i} \quad f : \Pi A \;B \quad a : A\\
\hline
f a : B[x \mapsto a]
\end{array}$$
where $B[x \mapsto a]$ is the obvious capture-avoiding substitution. But in order to apply this rule (in the context $A : \mathsf{Type}_i$), we would need the conclusion that $A : \mathsf{Type} \vdash \lambda x . \mathsf{Type}_j : \Pi A (\lambda x . \mathsf{Type}_{j + 1})$.
But this is the very judgement we seek to derive. So in order to come up with a derivation of the judgement, we would need to have already derived the judgement. So clearly, the judgement can never be made.
Now clearly, it is possible to work around this if you're willing to dramatically alter the entire landscape of rules. For example, you could add a second, special elimination rule specifically for giving a type to terms of the form $(\lambda x : A . T) y$. But this ruins the harmonious structure of type checking in which there is only a single rule which can ever be the last one used in a typing judgement $x : Z$, since there will be two different elimination rules which can both cover the judgement $(\lambda x : A . T)y$.
A: I want to rework the answer given by @MarkSaving since I believe he is correct but I do not think his reasoning matches the type rules I had in mind. Hence, I will give an alternative path to show that formalizing $\Pi$ as a term is inadequate. Just to be clear, let's give some of our type rules using $\Pi$ as a term:
$$\cfrac{\Gamma\ ,\ x\ {:}\ \alpha\ {\vdash}\ B\ {:}\ \beta\ x}{\Gamma\ {\vdash}\ x\ {:}\ \alpha\ .\ B\ {:}\ \Pi\ \alpha\ \beta}\ \Pi\textit{-Intro}$$
$$\cfrac{\Gamma\ {\vdash}\ f\ {:}\ \Pi\ \alpha\ \beta\qquad\Gamma\ {\vdash}\ a\ {:}\ \alpha}{\Gamma\ {\vdash}\ f\ a\ {:}\ \beta\ a}\ \Pi\textit{-Elim}$$
We include an infinite cumulative hierarchy of universes: $\mathsf{Type}_0$, $\mathsf{Type}_1$, $\mathsf{Type}_2$, $\ldots$
$$\cfrac{\Gamma\ {\vdash}\ A\ {:}\ \alpha\qquad\Gamma\ {\vdash}\ \alpha'\ {:}\ \mathsf{Type}_i}{\Gamma\ {\vdash}\ A\ {:}\ \alpha'}\ \textit{Conv}\quad\text{if $\alpha=_\beta\alpha'$}$$
As claimed by @MarkSaving, we will also demonstrate that the following judgment is not derivable:
\begin{equation}
    \alpha\ {:}\ \mathsf{Type}_0\ {\vdash}\ x\ {:}\ \alpha\ .\ \mathsf{Type}_i\ {:}\ \Pi\ \alpha\ (\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ ) \tag{1}
\end{equation}
To derive (1), we need to use $\Pi$-Intro, which requires us to derive
\begin{equation}
    \alpha\ {:}\ \mathsf{Type}_0\ ,\ x\ {:}\ \alpha\ {\vdash}\ \mathsf{Type}_i\ {:}\ (\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ )\ x. \tag{2}
\end{equation}
Again, to derive (2), we need to use Conv (since $\mathsf{Type}_{i+1}=_\beta(\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ )\ x$), which requires us to derive
\begin{equation}
    \alpha\ {:}\ \mathsf{Type}_0\ ,\ x\ {:}\ \alpha\ {\vdash}\ (\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ )\ x\ {:}\ \mathsf{Type}_{i+2}. \tag{3}
\end{equation}
Finally, to derive (3), we need to use $\Pi$-Elim, which requires us to derive
\begin{equation}
    \alpha\ {:}\ \mathsf{Type}_0\ ,\ x\ {:}\ \alpha\ {\vdash}\ y\ {:}\ \alpha\ .\ \mathsf{Type}_{i+1}\ {:}\ \Pi\ \alpha\ (\ z\ {:}\ \alpha\ .\ \mathsf{Type}_{i+2}\ ). \tag{4}
\end{equation}
Notice that the right hand sides (of the turnstiles) of (4) and (1) are essentially the same. Hence, the above reasoning can be applied infinitely, requiring us to derive
\begin{equation}
    \alpha\ {:}\ \mathsf{Type}_0\ ,\ x_0\ {:}\ \alpha\ ,\ \ldots\ ,\ x_{n-2}\ {:}\ \alpha\ {\vdash}\ x_{n-1}\ {:}\ \alpha\ .\ \mathsf{Type}_j\ {:}\ \Pi\ \alpha\ (\ x_n\ {:}\ \alpha\ .\ \mathsf{Type}_{j+1}\ ) \tag{5}
\end{equation}
for higher and higher values of $j$ without terminating. Thus, by infinite descent, (1) is not derivable.
