[proofplan]
We unfold the ordinary function type as the dependent product over a family that is constant in the bound variable. Weakening turns the type judgment for $B$ over $\Gamma$ into a type judgment for $B^{\mathrm{const}}$ over $\Gamma,x:A$, so the dependent product formation rule applies. The introduction, elimination, beta, and optional eta rules are then obtained by specializing the corresponding dependent product rules to this constant family.
[/proofplan]
[step:Weaken $B$ to a constant family over $A$]
Since $\Gamma \vdash B\ \mathsf{type}$ and $\Gamma \vdash A\ \mathsf{type}$, weakening gives a type in the extended context
\begin{align*}
\Gamma,x:A \vdash B^{\mathrm{const}}\ \mathsf{type}.
\end{align*}
Here $B^{\mathrm{const}}$ denotes the weakened copy of $B$ in the context $\Gamma,x:A$; by construction, the displayed type expression contains no essential dependence on the variable $x$. This is exactly the constant family over $A$ with value $B$.
[guided]
The dependent product rule needs a type family in the extended context $\Gamma,x:A$. We begin only with
\begin{align*}
\Gamma \vdash B\ \mathsf{type},
\end{align*}
so we must first view $B$ as a type in the larger context where a fresh variable $x:A$ has been added. Since $\Gamma \vdash A\ \mathsf{type}$, the extended context $\Gamma,x:A$ is well formed. By the weakening principle, stated in [citetheorem:9622], the judgment for $B$ remains derivable after adjoining the unused variable $x:A$. Thus we obtain
\begin{align*}
\Gamma,x:A \vdash B^{\mathrm{const}}\ \mathsf{type}.
\end{align*}
The notation $B^{\mathrm{const}}$ records that this is not a new type former. It is the same type $B$, reindexed along the projection from the extended context $\Gamma,x:A$ back to $\Gamma$. Therefore $B^{\mathrm{const}}$ is a family over $A$ that does not vary with $x$.
[/guided]
[/step]
[step:Specialize dependent product formation to the constant family]
The dependent product formation rule says that from
\begin{align*}
\Gamma \vdash A\ \mathsf{type}
\end{align*}
and
\begin{align*}
\Gamma,x:A \vdash B^{\mathrm{const}}\ \mathsf{type}
\end{align*}
one derives
\begin{align*}
\Gamma \vdash \prod_{x:A} B^{\mathrm{const}}\ \mathsf{type}.
\end{align*}
The ordinary function type is introduced as the definitional abbreviation
\begin{align*}
A \to B \coloneqq \prod_{x:A} B^{\mathrm{const}}.
\end{align*}
Therefore its formation rule is precisely the dependent product formation rule in the special case where the codomain family is constant.
[/step]
[step:Specialize lambda introduction and application elimination]
For introduction, suppose that
\begin{align*}
\Gamma,x:A \vdash b(x):B^{\mathrm{const}}.
\end{align*}
The dependent product introduction rule gives
\begin{align*}
\Gamma \vdash \lambda x. b(x):\prod_{x:A}B^{\mathrm{const}}.
\end{align*}
Using the abbreviation $A \to B \coloneqq \prod_{x:A}B^{\mathrm{const}}$, this is exactly
\begin{align*}
\Gamma \vdash \lambda x. b(x):A \to B.
\end{align*}
For elimination, suppose that
\begin{align*}
\Gamma \vdash f:A \to B
\end{align*}
and
\begin{align*}
\Gamma \vdash a:A.
\end{align*}
Under the same identification, $f$ has type $\prod_{x:A}B^{\mathrm{const}}$. The dependent product elimination rule gives
\begin{align*}
\Gamma \vdash f(a):B^{\mathrm{const}}[a/x].
\end{align*}
Because $B^{\mathrm{const}}$ is the weakening of a type $B$ that does not depend on $x$, substitution of $a$ for $x$ yields the original type:
\begin{align*}
B^{\mathrm{const}}[a/x] \equiv B.
\end{align*}
Thus
\begin{align*}
\Gamma \vdash f(a):B.
\end{align*}
This is exactly the usual application rule for ordinary functions.
[/step]
[step:Specialize beta computation to ordinary function application]
Suppose that
\begin{align*}
\Gamma,x:A \vdash b(x):B^{\mathrm{const}}
\end{align*}
and
\begin{align*}
\Gamma \vdash a:A.
\end{align*}
The dependent product beta computation rule, as in [citetheorem:9627], gives
\begin{align*}
(\lambda x. b(x))(a) = b(a):B^{\mathrm{const}}[a/x].
\end{align*}
Since $B^{\mathrm{const}}[a/x] \equiv B$, this is the ordinary function beta rule
\begin{align*}
(\lambda x. b(x))(a) = b(a):B.
\end{align*}
[/step]
[step:Specialize eta only when the ambient product rules include eta]
Assume now that the ambient dependent product rule scheme includes eta for dependent products. If
\begin{align*}
\Gamma \vdash f:A \to B,
\end{align*}
then, under the identification $A \to B \coloneqq \prod_{x:A}B^{\mathrm{const}}$, the dependent product eta rule gives
\begin{align*}
f = \lambda x. f(x):\prod_{x:A}B^{\mathrm{const}}.
\end{align*}
This is exactly the specialized function eta rule
\begin{align*}
f = \lambda x. f(x):A \to B.
\end{align*}
In theories whose dependent product rules do not include eta, no such conclusion follows from the formation, introduction, elimination, and beta rules alone. This proves the stated conditional eta clause and completes the rule-by-rule identification of ordinary function types with constant dependent products.
[/step]
