Axiom Of Choice in DTT

AOC.agda

module AOC where

open import Agda.Builtin.Sigma 
open import Relation.Binary.PropositionalEquality using (_≡_;refl)

infix 0 _≈_
record _≈_ (A B : Set) : Set where
  field
    to   : A → B
    from : B → A
    from∘to : ∀ (x : A) → from (to x) ≡ x
    to∘from : ∀ (y : B) → to (from y) ≡ y
open _≈_

AOC : ∀ {I : Set} {J : I → Set} {X : (i : I) → J i → Set} → 
      (∀ (i : I) → Σ (J i) (λ j → (X i j))) ≈ (Σ (∀ (i : I) → J i) (λ ĵ → ∀ (i : I) → X i (ĵ i)))
AOC = record { 
  to = λ f → (λ i → fst (f i)) , λ i → snd (f i ) ; 
  from = λ sig → λ i → (fst sig) i , (snd sig) i ; 
  from∘to = λ x → refl; 
  to∘from = λ y → refl 
  }