The Coq mailing list

[Daniel Schepler <dschepler AT scalable-networks.com>]

I've written a Quotient.v file which defines quotient types along with 
induced 
functions from quotient types.  The main non-CiC axioms I use are 
Extensionality_Ensembles, proof_irrelevance, 
constructive_definite_description.  
It depends on several other of my files, for things like declaring implicit 
arguments in the Ensembles and Relation_Definitions libraries, defining a 
notation for specifying an Ensemble as you'd specify a sigma-type, etc.  If 
you want I can send Quotient.v and its dependencies in either a zip or a tar.
{gz,bz2,xz,...} file.

The main idea is: define

Definition equiv_class (x:A) : Ensemble A :=
  [ y:A | R x y ].
Definition equiv_classes : Ensemble (Ensemble A) :=
  Im Full_set equiv_class.
Definition quotient : Type :=
  { S:Ensemble A | In equiv_classes S }.
Definition quotient_projection : A -> quotient.
refine (fun a:A => exist _ (equiv_class a) _).
...
Defined.

Now if you have f : A -> B satisfying

forall a1 a2:A, R a1 a2 -> f a1 = f a2

then you prove

forall abar:quotient, exists! b:B, exists a:A,
  quotient_projection a = abar /\ f a = b.

Applying constructive_definite_description to this statement gives a function
forall abar:quotient, { b:B | exists a:A, quotient_projection a = abar /\ f a 
= b }.
It's easy to derive the induced function fbar : quotient -> B from this, and 
prove
forall a:A, fbar (quotient_projection a) = f a.

(I also provided variants for induced functions quotient R -> quotient S, 
quotient R -> quotient S -> C, quotient R -> quotient S -> quotient T.)
-- 
Daniel Schepler