Naive quotients of types?

Using Coq
1

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

2

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

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

4

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.

5

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