let pr1 : Π (A : Type) Π (B : A → Type) (Σ (a : A) B a) → A
≔ λA.λB. Σ-ind A B (λ_. A) (λa.λBa. a)
let pr2 : Π (A : Type) Π (B : A → Type) Π (s : Σ (a : A) B a) B (pr1 A B s)
≔ λA.λB. Σ-ind A B (λs. B (pr1 A B s)) (λa.λBa. Ba)