Proof scripts for the paper:
-Mathematical quotients and quotient types in Coq,
by
Laurent Chicli ,
Loic Pottier and
Carlos Simpson
of which here is the
version (ps)
of November 2002.
The proof scripts in
Coq
were written by
Laurent Chicli .
There are four files:
geuvers-coquand.v
quotient_false.v
Classic_AC_false_Type.v
Classic_AC_false_Set.v
The above scripts are from January 2003. Please refer to Laurent's page for the most
recent versions.