Why does the dependent product type need "forall"?

Question

I feel stupid asking this question because it is so fundamental to logic and math. However, in my starting to learn proof theory and now type theory, I have not seen an explanation on why you need the ∀ quantifier for dependent products. It seems like it can be left out / assumed. Let me explain.

Background

In section 4.2: Typing Rules and Dependent Products in Coq'Art: The Calculus of Inductive Constructions, they provide this definition of the dependent product type:

∀v:A,B is the type of the functions that map any v of type A to a term of type B where v may occur in B.

Then they provide the example:

Check le_n.
le_n : ∀n:nat, n ≤ n

So that example is saying

forall n of type natural number, n is less than or equal to n.

Problem

That makes sense, and it comes from how you would write it in classical logic proofs. However, I keep wondering why can't it just be written like this:

Check le_n.
le_n n:nat : n ≤ n

That seems like it means the same thing to me. It means that

for all n of type natural number, n is less than or equal to n.

Or it feels to me it could mean "for any n", which may be different.

In both cases, you need some input to create the type, so it seems like they both mean "dependent type".

Basically, I'm just wondering why you have to include the forall ∀ in the definition (in Coq), when the fact that it's a definition means that it will apply to all cases anyways. Any thoughts?

Answer 1

Well, it turns out the type of le_n is indeed a dependent product:

le_n : ∀ (n : nat), n ≤ n

The fact that it is displayed as a function with named arguments is syntactic sugar. In fact, when I check le_n in my version of Coq it displays this:

le_n
     : forall n : nat, n <= n

And whenever you write something like this:

Definition f (a1 : T1) (a2 : T2) : T3 -> T4 := ...

Your are really declaring:

Definition f : ∀ (a1 : T1) (a2 : T2), T3 -> T4 := λ a1 a2 → ...