# Equivalence relations and quotients

Set Implicit Arguments.

Require Import Extensionality.

Implicit Type X Y Z W : Set.

## Equivalence relations

Record Eqv (X : Set) : Type := {
eqv_data :> XXProp;
eqv_rfl : x, eqv_data x x;
eqv_sym : x y, eqv_data y xeqv_data x y;
eqv_trs : x y z,
eqv_data x yeqv_data y zeqv_data x z
}.

Hint Immediate eqv_sym.
Hint Resolve eqv_rfl eqv_trs.

Lemma eq_eqv : X (r : Eqv X) x y, x = yr x y.
Proof.
destruct 1. apply eqv_rfl.
Qed.

Hint Resolve eq_eqv.

## Quotients

Parameter quotient : (X : Set) (r : Eqv X), Set.
Implicit Arguments quotient [].
Infix "//" := quotient
(at level 45, right associativity) : quotient.
Open Scope quotient.

Parameter class : (X : Set) (r : Eqv X), XX//r.
Implicit Arguments class [X].
Notation "x / r" := (class r x) : quotient.

Axiom class_eq : (X : Set) (r : Eqv X) (x y : X),
r x yx/r = y/r.
Hint Resolve class_eq.

Axiom class_rel : (X : Set) (r : Eqv X) (x y : X),
x/r = y/rr x y.
Hint Resolve class_rel.

Axiom class_ind : (X : Set) (r : Eqv X) (P : X // rProp),
( x : X, P (x / r)) → x : X // r, P x.

Parameter factor : (X : Set) (r : Eqv X) Y (f : XY)
(Hf : x y, r x yf x = f y),
X//rY.
Implicit Arguments factor [X Y].

Axiom factorize : (X : Set) (r : Eqv X) (Y : Set) (f : XY)
(H : x y, r x yf x = f y),
x , factor r f H (x/r) = f x.
Hint Resolve factorize.
Hint Rewrite factorize : quotient.

Lemma factor_extens : X (r : Eqv X) Y (f g : XY)
(Hf : x y, r x yf x = f y)
(Hg : x y, r x yg x = g y)
(H : x, f x = g x),
x, factor r f Hf x = factor r g Hg x.
Proof.
intros.
apply (class_ind (fun xfactor r f Hf x = factor r g Hg x)).
intros.
do 2 rewrite factorize. trivial.
Qed.

Definition frel X Y (r : Eqv Y) (f g : XY) : Prop :=
x, r (f x) (g x).

Definition feqv X Y (r : Eqv Y) : Eqv (XY).
Proof.
intros.
split with (@frel X Y r);
abstract (unfold frel; simpl; trivial; firstorder eauto).
Defined.

Definition theta' X Y (r : Eqv Y) : (XY) → (XY // r) :=
fun f xf x / r.

Lemma theta'_compat : X Y (r : Eqv Y) (f g : XY),
feqv X r f gtheta' r f = theta' r g.
Proof.
simpl. intros. unfold theta'.
apply extensionality. auto.
Qed.

Definition theta X Y (r : Eqv Y) : (XY) // feqv X rXY // r :=
fun (f : (XY) // feqv X r) (x : X) ⇒
factor (feqv X r) (@theta' X Y r) (@theta'_compat X Y r) f x.

Axiom theta_surj : X Y (r : Eqv Y) (f : XY // r),
h : (XY) // feqv X r, f = theta h.

Lemma lift_fun : X Y (r : Eqv Y) (f : XY // r),
h : XY, f = fun xh x / r.
Proof.
intros.
destruct (theta_surj f) as [h Hh].
generalize h Hh. clear h Hh.
apply (class_ind
(fun hf = theta h h0 : XY, f = (fun x : Xh0 x / r))).
intros g Hg.
g.
subst f.
apply extensionality.
unfold theta.
intros.
rewrite factorize.
reflexivity.
Qed.

Ltac lift_fun f g :=
destruct (lift_fun f) as [g Hlift_f]; subst f.

Section Factor1.

Variable (X : Set) (rX : Eqv X) (Y : Set) (rY : Eqv Y) (f : XY).
Hypothesis Hf : x y, rX x yrY (f x) (f y).

Definition factor1 : X // rXY // rY.
Proof.
apply (factor rX (fun xf x / rY)).
abstract auto.
Defined.

Lemma factorize1 : x, factor1 (x / rX) = f x / rY.
Proof.
unfold factor1.
intros. rewrite factorize. reflexivity.
Qed.

End Factor1.

Implicit Arguments factor1 [X Y].
Implicit Arguments factorize1 [X Y].
Hint Rewrite factorize1 : quotient.

Lemma factor1_extens : X (rX : Eqv X) Y (rY : Eqv Y) (f g : XY)
(Hf : x y, rX x yrY (f x) (f y))
(Hg : x y, rX x yrY (g x) (g y))
(H : x, rY (f x) (g x)),
x, factor1 rX rY f Hf x = factor1 rX rY g Hg x.
Proof.
intros. unfold factor1.
apply factor_extens. auto.
Qed.

Section Factor2.

Variable (X : Set) (rX : Eqv X) (Y : Set) (rY : Eqv Y) (Z : Set) (rZ : Eqv Z).
Variable f : XYZ.

Hypothesis Hf : x y z w,
rX x yrY z wrZ (f x z) (f y w).

Let h (x : X) : Y // rYZ // rZ.
Proof.
apply (factor1 rY rZ (f x)). abstract auto.
Defined.

Remark rmk : x y, rX x yh x = h y.
Proof.
unfold h. intros. apply extensionality.
apply (class_ind
(fun x0
factor1 rY rZ (f x) (h_subproof x) x0 = factor1 rY rZ (f y) (h_subproof y) x0)).
intros.
do 2 rewrite factorize1. auto.
Qed.

Definition factor2 : X // rXY // rYZ // rZ.
Proof.
apply (factor rX h). exact rmk.
Defined.

Lemma factorize2 : x y,
factor2 (x / rX) (y / rY) = f x y / rZ.
Proof.
unfold factor2, h. intros.
rewrite factorize. rewrite factorize1. auto.
Qed.

End Factor2.

Implicit Arguments factor2 [X Y Z].
Implicit Arguments factorize2 [X Y Z].

Hint Rewrite factorize2 : quotient.

Lemma factor2_extens :
X (rX : Eqv X) Y (rY : Eqv Y) Z (rZ : Eqv Z)
(f : XYZ)
(Hf : x y z w, rX x yrY z wrZ (f x z) (f y w))
(g : XYZ)
(Hg : x y z w, rX x yrY z wrZ (g x z) (g y w))
(H : x y, rZ (f x y) (g x y)) x y,
factor2 rX rY rZ f Hf x y = factor2 rX rY rZ g Hg x y.
Proof.
intros until 1.
apply (class_ind
(fun x (y : Y // rY),
factor2 rX rY rZ f Hf x y = factor2 rX rY rZ g Hg x y)).
intro.
apply (class_ind
(fun yfactor2 rX rY rZ f Hf (x/rX) y = factor2 rX rY rZ g Hg (x/rX) y)).
intro. do 2 rewrite factorize2. auto.
Qed.