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