Hello,

Trying to transport my set-theoretical intuition to Coq, I tried to define the quotient of a type by an equivalence relation, but I cannot figure out how to prove the universal property of the quotient. Details below. Any comments/suggestions welcome!

```
(* Types ~ Sets *)
Parameter X Y : Type.
(* P X ~ Power set *)
Definition P (X : Type) : Type := X -> Prop.
(* An equivalence relation on X *)
Parameter R : X -> X -> Prop.
(* IsOrb U : whether U corresponds to an orbit of the relation R *)
Definition IsOrb (U : P X) : Prop := exists x : X, forall y, U y <-> R x y.
(* Definition of the "naive" quotient of X by R *)
Definition X_R := { U : P X | IsOrb U }.
(* Definition of the projection pi : X -> X_R *)
Require Import Program.
Program Definition pi : X -> X_R := R.
Next Obligation.
unfold IsOrb. exists x. intros. apply iff_refl.
Qed.
(* Haven't worked out all the details of uniqueness part of
universal property for pi, but looks doable. *)
Lemma uniqueness: forall g h : X_R -> Y,
(forall x : X, g (pi x) = h (pi x)) ->
forall x' : X_R, g x' = h x'.
Admitted.
(* Cannot see how to prove existence part of universal
property for pi. *)
Lemma existence: forall f : X -> Y,
(forall x y : X, R x y -> f x = f y) ->
exists f' : X_R -> Y, forall x, f' (pi x) = f x.
Admitted.
```

Thanks!

Best wishes,

Nicolás