I'm trying to implement the sigma elimination as via the induction principle, and am not understanding why pr₂ is fine, but pr₂' is highlighting yellow with the constraint error below, as these programs are eta equivalent. This is not the case with pr₁ and pr₁'.
Will you please explain the error, and additionally why agda only likes pr₂, doesn't accept pr₂', and meanwhile accepts both pr₁ and pr₁'. [Disclaimer: some of this code is Egbert Rijke's from his course at 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]