Question regarding sigma type signature

Stream: new members

[Rajiv]

In Theorem Proving in Lean, Section 7.2, https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html#constructors-with-arguments , there is an example for defining sigma types.

universes u v

inductive sigma₁ {α : Type u} (β : α → Type v)
| dpair : Π a : α, β a → sigma₁

#check @sigma₁

#check @sigma₁.dpair

The type signature for sigma₁.dpair is shown as follows.

sigma₁.dpair : Π {α : Type u_1} {β : α → Type u_2} (a : α), β a → sigma₁ β

I was wondering why dpair is generating term of type sigma₁ β and not sigma₁ α β?

[Mario Carneiro]

the alpha is implicit

[Mario Carneiro]

because it was written {α : Type u}

[Rajiv]

Thanks Mario. Now I see it.