Agda pattern matching inside type declarations

Question

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

gallais gallais · Accepted Answer · 2020-03-06T16:15:28

The ability to pattern-match on records in telescopes will be available in the (soon) upcoming version Agda 2.6.1.

Cf. the documentation of the development branch: https://agda.readthedocs.io/en/latest/language/telescopes.html#irrefutable-patterns-in-binding-positions

Agda pattern matching inside type declarations

1 Answers