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)