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.