Require Import overture pext inhab fext.

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

  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.

  Definition quot : Type := { P : Pred A & hexists x : A, conv x = P }.

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

  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.

  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.

  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.

  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.

  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.

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.