Agda pattern matching inside type declarations

I am learning HoTT with Agda form beginning. I followed instructions in https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/

When I started to type in declaration of dependent sum type induction just like the notes instructed,

record Σ { } {X :  ̇ } (Y : X →  ̇ ) :  ⊔  ̇  where
  constructor _,_
  field
    x : X
    y : Y x

pr₁ : {X :  ̇ } {Y : X →  ̇ } → Σ Y → X
pr₁ (x , y) = x

pr₂ : {X :  ̇ } {Y : X →  ̇ } → (z : Σ Y) → Y (pr₁ z)
pr₂ (x , y) = y


Σ-induction : {X :  ̇ } {Y : X →  ̇ } {A : Σ Y →  ̇ }
            → ((x : X) (y : Y x) → A (x , y))
            → ((x , y) : Σ Y) → A (x , y)

Σ-induction g (x , y) = g x y

My agda said there's an error with code → ((x , y) : Σ Y):

expected sequence of possibly hidden bound identifiers

And when I change my type declaration like:

Σ-induction : {X :  ̇ } {Y : X →  ̇ } {A : Σ Y →  ̇ }
            → ((x : X) (y : Y x) → A (x , y))
            → (z : Σ Y) → A (pr₁ z , pr₂ z)

Σ-induction g (x , y) = g x y

This version is fine.

So I'm wondering that if the problem is that agda do not support pattern matching inside type declarations.

p.s. I'm using Agda 2.6.0.1