# Quotients in Coq

Quotients are crucial in mathematical practice, and it is a shame that they
are not available in Coq's standard library. There was a recent discussion on
the Coq GitHub page on
this issue and the consequences of implementing quotients like Lean does, where the eliminator for
function types has a reduction rule that breaks pleasant metatheoretic
properties such as subject reduction.
In this post, we are going to define quotients in Coq with three standard
axioms:

- Functional extensionality
- Propositional extensionality
- Constructive definite description (also known as the axiom of unique choice)

Check @functional_extensionality_dep :

∀ A B (f g : ∀ x : A, B x),

(∀ x : A, f x = g x) → f = g.

Check @propositional_extensionality :

∀ P Q, (P ↔ Q) → P = Q.

Check @constructive_definite_description :

∀ A P, (exists! x : A, P x) → {x : A | P x}.

As far as axioms go, these three are relatively harmless. In particular,
they are valid in any elementary
topos, which are generally regarded as a good universe for doing
constructive, higher-order reasoning. (Naturally, adding axioms in type theory
does not come for free: since they have no useful reduction behavior, our
quotients won't compute.)

Section Quotient.

We define the quotient of T by an equivalence relation R as usual: it is
the type of equivalence classes of R.

Context (T : Type) (R : relation T) (RP : Equivalence R).

Record quot := Quot_ {

quot_class : T → Prop;

quot_classP : ∃ x, quot_class = R x;

}.

The projection into the quotient is given by the Quot constructor below,
which maps x to its equivalence class R x. This definition satisfies the
usual properties: Quot x = Quot y if and only if R x y. The "if" direction
requires the principle of proof irrelevance, which is a consequence of
propositional extensionality.

Definition Quot (x : T) : quot :=

@Quot_ (R x) (ex_intro _ x erefl).

Lemma Quot_inj x y : Quot x = Quot y → R x y.

Proof.

move=> e; rewrite -[R x y]/(quot_class (Quot x) y) e //=; reflexivity.

Qed.

Lemma eq_Quot x y : R x y → Quot x = Quot y.

Proof.

move=> e; rewrite /Quot; move: (ex_intro _ y _).

suff ->: R y = R x.

move=> ?; congr Quot_; exact: proof_irrelevance.

apply: functional_extensionality=> z.

apply: propositional_extensionality.

by rewrite /= e.

Qed.

We can also show that Quot is surjective by extracting the witness in the
existential.

Lemma Quot_inv q : ∃ x, q = Quot x.

Proof.

case: q=> [P [x xP]]; exists x; move: (ex_intro _ _ _).

rewrite xP=> e; congr Quot_; exact: proof_irrelevance.

Qed.

Proof.

case: q=> [P [x xP]]; exists x; move: (ex_intro _ _ _).

rewrite xP=> e; congr Quot_; exact: proof_irrelevance.

Qed.

Unique choice comes into play when defining the elimination principles for
the quotient. In its usual non-dependent form, the principle says that we can
lift a function f : T → S to another function quot → S provided that f is
constant on equivalence classes. We define a more general dependently typed
version, which allows in particular to prove a property S q by proving that S
(Quot x) holds for any x. The statement of the compatibility condition for
f is a bit complicated because it needs to equate terms of different types S
(Quot x) and S (Quot y), which requires us to transport the left-hand side
along the equivalence R x y.

Section Elim.

Definition cast A B (e : A = B) : A → B :=

match e with erefl => id end.

Context (S : quot → Type) (f : ∀ x, S (Quot x)).

Context (fP : ∀ x y (exy : R x y), cast (congr1 S (eq_Quot exy)) (f x) = f y).

We begin with an auxiliary result that uniquely characterizes the result of
applying the eliminator to an element q : quot. Thanks to unique choice, this
allows us to define the eliminator as a function quot_rect.

Lemma quot_rect_subproof (q : quot) :

exists! a : S q, ∃ x (exq : Quot x = q), a = cast (congr1 S exq) (f x).

Proof.

case: (Quot_inv q)=> x -> {q}.

exists (f x); split=> [|a]; first by exists x, erefl.

case=> y [eyx -> {a}].

by rewrite (proof_irrelevance _ eyx (eq_Quot (Quot_inj eyx))) fP.

Qed.

Definition quot_rect q : S q :=

sval (constructive_definite_description _ (quot_rect_subproof q)).

Lemma quot_rectE x : quot_rect (Quot x) = f x.

Proof.

rewrite /quot_rect.

case: constructive_definite_description=> _ [y [eyx /= ->]].

by rewrite (proof_irrelevance _ eyx (eq_Quot (Quot_inj eyx))) fP.

Qed.

End Elim.

In the non-dependent case, the compatibility condition acquires its usual
form.

Section Rec.

Context S (f : T → S) (fP : ∀ x y, R x y → f x = f y).

Definition congr1CE (A B : Type) (b : B) x y (e : x = y) :

congr1 (λ _ : A, b) e = erefl :=

match e with erefl => erefl end.

Definition quot_rec : quot -> S :=

@quot_rect (λ _, S) f

(λ x y exy, etrans

(congr1 (λ p, cast p (f x)) (congr1CE S (eq_Quot exy)))

(fP exy)).

Lemma quot_recE x : quot_rec (Quot x) = f x.

Proof. by rewrite /quot_rec quot_rectE. Qed.

End Rec.

End Quotient.