Problems with the Dependent cartesian product example

Stream: lean4

[Stefano]

In the dependent cartesian product example, there is this snippet:

universe u v

def f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
  ⟨a, b⟩

If I rewrite it like this:

variable (α : Type u)
variable (β : α → Type v)
def f (a : α)(b: β a) : (a : α) × (b : β a) := ⟨a, b⟩

I got an error on the b type, but I don't understand why and the message is pretty cryptic:

type mismatch
b
has type
β a : Type v
but is expected to have type
β a : Type v

Anyone can help me out here, please?

[Tomas Skrivan]

You have a typo there, the type after colon : should not be (a : α) × (b : β a) but : (a : α) × (β a).