# Quotients

We first define quotients by equivalence relations and then lift this to quotients by arbitrary relations.
Require Import overture pext inhab fext.

## Relation Quotient Types

Section QuotientTypes.
Variables (A : Type) (R : Rel A).

Equivalence closure of R
Inductive conv x : Pred A :=
| convxx : conv x x
| conv1S y z : R y z -> conv x y -> conv x z
| conv1R y z : R z y -> conv x y -> conv x z.

Instance: Reflexive conv.
Proof. exact: convxx. Qed.

Instance: Transitive conv.
Proof. move=> x y z cxy cyz. elim: cyz; eauto using conv. Qed.

Instance: Symmetric conv.
Proof.
move=> x y. elim=>{y}. exact: convxx.
- move=> y z ryz _ cyx. transitivity y; eauto using conv.
- move=> y z rzy _ cyx. transitivity y; eauto using conv.
Qed.

Instance: Equivalence conv.
Proof. constructor; exact _. Qed.

The quotient of A by R is the type of inhabited equivalence classes of R.
Definition quot : Type := { P : Pred A & hexists x : A, conv x = P }.

Representative of x
Definition repr x : quot := (conv x; tr (x; erefl)).

Paths between representatives
Lemma conv_repr {x y} (cxy : conv x y) : repr x = repr y.
Proof. apply: tag_injective. fext=>/=z. apply: pext => []<-//. by symmetry. Qed.

Lemma reprP {x y} (rxy : R x y) : repr x = repr y.
Proof. apply: conv_repr; eauto using conv. Qed.

Existence of representatives
Lemma repr_surjective : surjective repr.
Proof.
case=> P. inhab=> x E /=. apply: tr. exists x.
apply: sigT_eq. by destruct E.
Defined.

Lemma exists_repr q : exists x, repr x = q.
Proof.
move: (repr_surjective q). apply: inhab_ind => /=; by firstorder.
Defined.

Lifting of respectful functions
Program Definition quot_rec {B : Type} (f : A -> B)
(fP : forall x y, R x y -> f x = f y) (q : quot) : B :=
inhab_rec (fun p => f p.1) _ q.2.
Next Obligation.
suff H: forall x y, conv x y -> f x = f y.
- apply: H => /=. rewrite X0 -X. exact: convxx.
- move=> {x X0 y X} x y. by elim=> //{y}[y z /fP->_->|y z /fP->_->].
Qed.
Arguments quot_rec {B} f fP q.

Induction
Section Induction.
Variable P : quot -> Type.
Variable f : forall x, P (repr x).
Hypothesis fP : forall x y (r : R x y), reprP r # f x = f y.

Program Definition quot_rect_total : quot -> { q' : quot & P q' } :=
quot_rec (fun x => (repr x; f x)) _.
Next Obligation.
apply: sigT_eq (reprP H) _. exact: fP.
Defined.

Definition quot_rect_total_id (q : quot) : (quot_rect_total q).1 = q.
Proof. destruct (exists_repr q). subst. reflexivity. Defined.

Definition quot_rect (q : quot) : P q :=
quot_rect_total_id q # (quot_rect_total q).2.

Lemma quot_rectE x : quot_rect (repr x) = f x. by []. Qed.
End Induction.

Definition quot_ind (P : quot -> hprop) (f : forall x, P (repr x)) : forall q, P q.
Proof. apply: (quot_rect (f := f)) => x y rxy. exact: hpropP. Defined.

Paths in quotients
Section Paths.
Program Definition in_class x : quot -> Prop :=
quot_rec (conv x) _.
Next Obligation.
move: x0 y H => y z ryz. apply: pext=> [rxy|rxz].
exact: conv1S ryz _. exact: conv1R ryz _.
Qed.

Lemma in_classE x y :
in_class x (repr y) = conv x y.
Proof. by []. Qed.

Lemma repr_conv x y :
repr x = repr y <-> conv x y.
Proof.
split=> [eqn|]. rewrite -in_classE -eqn /=. exact: convxx.
elim=> //{y}[y z ryz _->|y z ryz _->]; by rewrite (reprP ryz).
Qed.
End Paths.

(* If R is an equivalence, then it is equal to conv. *)
Context `{Equivalence A R}.

Lemma conv_equiv x y :
conv x y <-> R x y.
Proof.
split; last first. move=> /conv1S. apply. exact: convxx.
elim=>{y}. reflexivity. move=> y z ryz _ rxy. by transitivity y.
move=> y z ryz _ rxy. transitivity y => //. by symmetry.
Qed.

Lemma repr_equiv x y : repr x = repr y <-> R x y.
Proof. by rewrite repr_conv conv_equiv. Qed.
End QuotientTypes.
Arguments repr {A} R x, {A R} x.
Arguments quot_rec {A R B} f fP q.
Arguments quot_ind {A R} P f q.

Definition quot_rec2 {A B C : Type} {R : Rel A} {S : Rel B} (f : A -> B -> C) :
(forall x y1 y2, S y1 y2 -> f x y1 = f x y2) ->
(forall x1 x2 y, R x1 x2 -> f x1 y = f x2 y) ->
quot R -> quot S -> C.
Proof.
move=> h1 h2. apply: (quot_rec (fun x => quot_rec (f x) (h1 x)) _).
abstract (move=>/=x y rxy; fext=> q; case: (exists_repr q) => z<-/=; exact: h2).
Defined.
Arguments quot_rec2 {A B C R S} f h1 h2 x y : rename.

## Characterization of maps out of quotients

Section QuotientMappingProperty.
Variables (A B : Type) (R : Rel A).

Definition quot_map (f : quot R -> B) : { f : A -> B | forall x y, R x y -> f x = f y }.
Proof.
refine (exist _ (f \o repr) _). move=> x y r /=. exact: (ap f (reprP r)).
Defined.

Definition map_quot (p : { f : A -> B | forall x y, R x y -> f x = f y }) : quot R -> B :=
quot_rec p.1 p.2.

Lemma quot_map_sect (f : quot R -> B) : map_quot (quot_map f) = f.
Proof. fext. exact: quot_ind. Qed.

Lemma quot_map_retr p : quot_map (map_quot p) = p.
Proof. exact: sig_eq. Qed.

Definition quot_map_is_equiv : is_equiv quot_map :=
mk_is_equiv map_quot quot_map_sect quot_map_retr.

Canonical quot_map_equiv := mk_equiv quot_map quot_map_is_equiv.
End QuotientMappingProperty.