Theorem of Choice in Agda

gistfile1.agda

module Choice where

record Σ(A : Set)(P : A → Set) : Set where
  field
    fst : A
    snd : P fst

choice : {A : Set}{R : A → A → Set} →
         ((n : A) → Σ A (λ m → R n m)) →
         Σ (A → A) (λ f → (
         (n : A) → R n (f n))) 
choice g = record { fst = λ x → Σ.fst (g x); snd = λ y → Σ.snd (g y) }