The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Wed, Nov 9, 2011 at 10:28 AM,  <roconnor AT theorem.ca> wrote:

I'm not sure why Schepler suggested that he only used the
Ensembles.Extensionality axiom.  This doesn't appear to be the case to me. I may be misunderstanding something here.

OK, so maybe I didn't enumerate all the necessary axioms.  I was just going from memory and identifying what seemed to me (subjectively) to be the most "objectionable" axioms that I used in that file.  Although, I still considered it to fall short of fully classical reasoning -- it can construct quotients just fine within the sheaves/topos model of type theory.
--
Daniel Schepler