Agda сопоставление шаблонов внутри объявлений типов - PullRequest
Новая
       13

Agda сопоставление шаблонов внутри объявлений типов

1 голос
/ 06 марта 2020

Я изучаю HoTT с начала формы Agda. Я следовал инструкциям в https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/

Когда я начал вводить декларацию индукции типа зависимой суммы, точно так же, как в инструкциях, 

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

Моя агда сказала, что есть ошибка с кодом → ((x , y) : Σ Y): 

expected sequence of possibly hidden bound identifiers

И когда я меняю объявление типа, например: 

Σ-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

Эта версия в порядке.

Так что я интересно, если проблема в том, что agda не поддерживает сопоставление с образцом внутри объявлений типов.

ps Я использую Agda 2.6.0.1

1 Ответ

1 голос
/ 06 марта 2020

Возможность сопоставления с образцом на записях в телескопах будет доступна в (скорой) следующей версии Agda 2.6.1.

Cf. документация ветки разработки: https://agda.readthedocs.io/en/latest/language/telescopes.html#irrefutable -pattern-in-binding-положений

...