# Naive quotients of types?

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'.

(* 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.
``````

Thanks!
Best wishes,
Nicolás

A classic problem. Here is the outline of my solution:

``````Parameter R_refl : forall x, R x x.
Parameter R_symm : forall x y, R x y -> R y x.

Definition member (xr : X_R) (x : X) : Prop :=
let (p, _) := xr in
p x.

Lemma member_pi : forall x y, member (pi x) y <-> R x y.

Require Import Coq.Logic.ClassicalChoice.
Lemma Projection : exists (f : X_R -> X), forall (xr : X_R), member xr (f xr).
Proof.
apply (choice member).
(* ... *)
Qed.

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.
Proof.
intros f Hf.
destruct Projection as [proj Hproj].
exists (fun xr => f (proj xr)).
(* ... *)
Qed.
``````

Hello @gasche ,

Thanks for your answer! If I understand correctly, your solution is based on constructing a section of `pi` by using the axiom of choice. I see that the reference to the existence of some kind of “choice” function is very much present in the usual set-theoretic setting as well, but is typically not made explicit.

Best wishes,
Nicolás

The main reason I needed choice here (but maybe it’s possible to do without) is because the point of the orbit is hidden in an `exists` quantifier in your definition, so extracting it would require eliminating from Prop to Type. I have an easier solution, without choice, when using a definition where this point is directly in Type:

``````Record X_R := { p : P X; x : X; orb : forall y, p y <-> R x y }.
``````

On the other hand, if your mental model includes functional extensionality and prop-irrelevance, then your previous definition would give a notion of propositional equality on `X_R` that is rather natural (same equivalence class), while here you want to define a relation that ignores the `x` to compare those objects.

To define quotients, you actually don’t need to construct the section of the projection. I wrote a post (http://poleiro.info/posts/2019-12-25-quotients-in-coq.html) explaining how the axiom of unique choice, a weaker variant of the axiom of choice suffices (together with propositional and functional extensionality):

``forall T (P : T -> Prop), (exists! x, P x) -> {x : T | P x}.``