如何推断两个具有不同行为的 eta 等效 agda 程序？

问：

我正在尝试通过感应原理实现西格玛消除，但我不明白为什么很好，但在下面用约束误差突出显示黄色，因为这些程序是等效的。pr₁ 和 pr₁' 并非如此。pr₂pr₂'

请您解释一下错误，以及为什么 agda 只喜欢 ，不接受 pr₂'，同时同时接受 pr₁ 和 pr₁'。[免责声明：其中一些代码是 Egbert Rijke 在 CMU 课程中的代码]pr₂

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]