# Naive quotients of types?

**URL:** <https://discourse.rocq-prover.org/t/naive-quotients-of-types/882>\
**Category:** Using Rocq\
**Created:** [June 11, 2020, 1:42am UTC](https://discourse.rocq-prover.org/t/naive-quotients-of-types/882 "2020-06-11T01:42:34Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![nojb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nojb/32/256_2.png) [@nojb](https://discourse.rocq-prover.org/u/nojb)\
**Post date:** [June 11, 2020, 1:42am UTC](https://discourse.rocq-prover.org/t/naive-quotients-of-types/882/1 "2020-06-11T01:42:34Z")

</div>

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!

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

---

<div class="post-metadata">

**Author:** ![gasche](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/gasche/32/16_2.png) [@gasche](https://discourse.rocq-prover.org/u/gasche)\
**Post date:** [June 11, 2020, 9:07am UTC](https://discourse.rocq-prover.org/t/naive-quotients-of-types/882/2 "2020-06-11T09:07:48Z")

</div>

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

```auto
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.  

```

---

<div class="post-metadata">

**Author:** ![nojb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nojb/32/256_2.png) [@nojb](https://discourse.rocq-prover.org/u/nojb)\
**Post date:** [June 11, 2020, 9:33am UTC](https://discourse.rocq-prover.org/t/naive-quotients-of-types/882/3 "2020-06-11T09:33:28Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![gasche](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/gasche/32/16_2.png) [@gasche](https://discourse.rocq-prover.org/u/gasche)\
**Post date:** [June 11, 2020, 9:50am UTC](https://discourse.rocq-prover.org/t/naive-quotients-of-types/882/4 "2020-06-11T09:50:53Z")

</div>

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:

```coq
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.

---

<div class="post-metadata">

**Author:** ![arthuraa](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/arthuraa/32/297_2.png) [@arthuraa](https://discourse.rocq-prover.org/u/arthuraa)\
**Post date:** [June 17, 2020, 4:29pm UTC](https://discourse.rocq-prover.org/t/naive-quotients-of-types/882/5 "2020-06-17T16:29:57Z")

</div>

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](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}.
```