Как можно объяснить две эти-эквивалентные программы agda с различным поведением? - PullRequest
Новая
       86

Как можно объяснить две эти-эквивалентные программы agda с различным поведением?

2 голосов
/ 03 апреля 2020

Я пытаюсь реализовать устранение сигмы, используя принцип индукции, и я не понимаю, почему pr₂ нормально, но pr₂' выделяет желтый цвет с ошибкой ограничения ниже, так как эти программы являются эквивалентными. Это не относится к pr₁ и pr₁ '.

Пожалуйста, объясните ошибку и, кроме того, почему agda любит только pr₂, не принимает pr₂' и тем временем принимает оба pr₁ и pr₁ '. [Отказ от ответственности: часть этого кода Эгберта Рийке из его курса в CMU] 

open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) public

UU : (i : Level) → Set (lsuc i)
UU i = Set i

data Σ {i j : Level} (A : UU i) (B : A → UU j) : UU (i ⊔ j) where
  pair : (x : A) → (B x → Σ A B)

ind-Σ : {i j k : Level} {A : UU i} {B : A → UU j} {C : Σ A B → UU k} →
  ((x : A) (y : B x) → C (pair x y)) → ((t : Σ A B) → C t)
ind-Σ f (pair x y) = f x y

pr₁ : {i j : Level} {A : UU i} {B : A → UU j} → Σ A B → A
pr₁ x = ind-Σ (λ x y → x) x

pr₁' : {i j : Level} {A : UU i} {B : A → UU j} → Σ A B → A
pr₁' = ind-Σ (λ x y → x) 

pr₂ : {i j : Level} { A : UU i } { B : A → UU j } → (t : Σ A B) → B (pr₁ t)
pr₂ = ind-Σ (λ x y → y) 

pr₂' : {i j : Level} { A : UU i } { B : A → UU j } → (t : Σ A B) → B (pr₁ t)
pr₂' f = ind-Σ (λ x y → y) f

-- ———— Errors ————————————————————————————————————————————————
-- Failed to solve the following constraints:
-- _196
-- := λ {i} {j} {A} {B} f →
-- ind-Σ (λ x y → _195 (f = f) (x = x) (y = y)) f
-- [blocked on problem 399]
-- [399] _C_193 f =< B (pr₁ f) : Set j
-- [393] B x =< _C_193 (pair x y) : Set j
-- _194 := λ {i} {j} {A} {B} f x y → y [blocked on problem 393]
...