0

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?

Eben Kadile
  • 732
  • 4
  • 16

1 Answers1

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)).
Daniel Schepler
  • 20,364
  • (Incidentally, I think even considering only constructive functions, the axiom of choice does become nontrivial again if you consider the category of setoids (or should that be typeoids?) rather than the category of types.) – Daniel Schepler Feb 15 '18 at 02:27