This module states the functional form of the axiom of choice over
setoids, commonly called extensional axiom of choice
[Carlström04],
[Martin-Löf05]. This is obtained by a decomposition of the axiom
into the following components:
- classical logic
- relational axiom of choice
- axiom of unique choice
- a limited form of functional extensionality
Among other results, it entails:
- proof irrelevance
- choice of a representative in equivalence classes
[Carlström04] Jesper Carlström, EM + Ext + AC_int is equivalent to
AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004.
[Martin-Löf05] Per Martin-Löf, 100 years of Zermelo’s axiom of
choice: what was the problem with it?, lecture notes for KTH/SU
colloquium, 2005.