# Library Rational.Quotient.quotient

Parameter MK_QUO : forall (A : Set) (R : A -> A -> Prop), Set.

Definition Compat (A : Set) (R : A -> A -> Prop) (B : Set)
(f : A -> B) := forall x y : A, R x y -> f x = f y.

Definition Compat_prop (A : Set) (R : A -> A -> Prop)
(P : A -> Prop) := forall x y : A, R x y -> (P x <-> P y).

Axiom
lift :
forall (A : Set) (R : A -> A -> Prop) (B : Set) (f : A -> B),
Compat A R B f -> MK_QUO A R -> B.

Axiom
lift_prop :
forall (A : Set) (R : A -> A -> Prop) (P : A -> Prop),
Compat_prop A R P -> MK_QUO A R -> Prop.

Parameter In : forall (A : Set) (R : A -> A -> Prop), A -> MK_QUO A R.

Axiom
From_R_to_L :
forall (A : Set) (R : A -> A -> Prop) (x y : A),
R x y -> In A R x = In A R y.

Axiom
From_L_to_R :
forall (A : Set) (R : A -> A -> Prop) (x y : A),
In A R x = In A R y -> R x y.

Axiom
Reduce :
forall (A : Set) (R : A -> A -> Prop) (B : Set)
(f : A -> B) (c : Compat A R B f) (a : A),
lift A R B f c (In A R a) = f a.

Axiom
Reduce_prop :
forall (A : Set) (R : A -> A -> Prop) (f : A -> Prop)
(c : Compat_prop A R f) (a : A), lift_prop A R f c (In A R a) = f a.

Axiom
Closure :
forall (A : Set) (R : A -> A -> Prop) (X : MK_QUO A R)
(P : MK_QUO A R -> Set), (forall x : A, P (In A R x)) -> P X.

Axiom
Closure_prop :
forall (A : Set) (R : A -> A -> Prop) (X : MK_QUO A R)
(P : MK_QUO A R -> Prop), (forall x : A, P (In A R x)) -> P X.

Axiom
Ext : forall (A B : Set) (f g : A -> B), (forall x : A, f x = g x) -> f = g.

Notation "| c |" := (In _ _ c) (at level 20, c at level 0).
Notation "c / c2" := (MK_QUO c c2).