Parameter MK_QUO : ∀ (A : Set) (R : A → A → Prop), Set.


Definition Compat (A : Set) (R : A → A → Prop) (B : Set)
  (f : A → B) := ∀ x y : A, R x y → f x = f y.


Definition Compat_prop (A : Set) (R : A → A → Prop)
  (P : A → Prop) := ∀ x y : A, R x y → (P x ↔ P y).


Axiom
  lift :
    ∀ (A : Set) (R : A → A → Prop) (B : Set) (f : A → B),
    Compat A R B f → MK_QUO A R → B.

Axiom
  lift_prop :
    ∀ (A : Set) (R : A → A → Prop) (P : A → Prop),
    Compat_prop A R P → MK_QUO A R → Prop.


Parameter In : ∀ (A : Set) (R : A → A → Prop), A → MK_QUO A R.


Axiom
  From_R_to_L :
    ∀ (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 :
    ∀ (A : Set) (R : A → A → Prop) (x y : A),
    In A R x = In A R y → R x y.


Axiom
  Reduce :
    ∀ (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 :
    ∀ (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 :
    ∀ (A : Set) (R : A → A → Prop) (X : MK_QUO A R)
      (P : MK_QUO A R → Set), (∀ x : A, P (In A R x)) → P X.


Axiom
  Closure_prop :
    ∀ (A : Set) (R : A → A → Prop) (X : MK_QUO A R)
      (P : MK_QUO A R → Prop), (∀ x : A, P (In A R x)) → P X.


Axiom
  Ext : ∀ (A B : Set) (f g : A → B), (∀ 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).