Proving the axiom of choice in propositions as types

Question

The axiom of choice can be stated as follows for a relation $R$ between terms of type $A$ and type $B$: $$(\forall x : A.\exists y: B.R\; x\; y) \rightarrow \exists f:A\rightarrow B.\forall x : A.R\; x\; (f\; x)$$ In proposition as types: $$ac:(\Pi_{x:A}\Sigma_{y:B}R\;x\;y)\rightarrow\Sigma_{f:A\rightarrow B}\Pi_{x:A}R\;x\;(f\;x)$$ Here's my attempt to define $ac$ by pattern matching on a dependent function $f$: $$ac\; f:= \;(fst\, \circ f,\; snd\,\circ f)$$ Where $fst$ gives the first component of a pair, and $snd$ gives the second. The output of this function has to be a non-dependent function paired with a dependent function. My reasoning is that the non-dependent function can be achieved by just projecting onto the first component of the output of $f$ because $f$ produces a pair with the first component satisfying the relation. Basically the same reasoning got me to the second component of the output.

This is pretty interesting stuff, and I intend on eventually installing Agda so that I can do lots of exercises and have them checked right away. But for now, is this correct?

Answer 1

It looks right to me. In Coq, this type checks:

Definition ac {A B:Type} {R:A->B->Type}
  (f : forall x:A, { y:B & R x y }) :
  { g:A->B & forall x:A, R x (g x) } :=
existT (fun g:A->B => forall x:A, R x (g x))
  (fun x => projT1 (f x))
  (fun x => projT2 (f x)).