Require Export Quotient_CR Embeddings.

(* Quotient construction assuming tree description (TD) and proof irrelevance (PI) *)

Parameter tdelta : (Acz -> Prop) -> Acz.

Axiom TDesc1 :
  forall P, (exists s, forall t, P t <-> Aeq t s) -> P (tdelta P).

Axiom TDesc2 :
  forall P P', (forall s, P s <-> P' s) -> tdelta P = tdelta P'.

(* The normaliser yielding the quotient model can be defined *)

Definition N s :=
  tdelta (Aeq s).

Axiom PI : forall s (H H' : N s = s), H = H'.

Fact CR1 :
  forall s, Aeq s (N s).
Proof.
  intros s. pattern (N s). apply TDesc1. now exists s.
Qed.

Lemma CR2 :
  forall s t, Aeq s t -> N s = N t.
Proof.
  intros s t H. apply TDesc2.
  intros u. rewrite H. tauto.
Qed.

Instance Norm : Normalizer :=
  @Build_Normalizer N CR1 CR2 PI.

(* This turns Acz into a model of intensional ZF *)

Instance ACZ : ZFStruct :=
  @Build_ZFStruct ACZ' tdelta.

Instance Acz_ZF :
  iZF ACZ.
Proof.
  split; try apply Acz_ZF'.
  - intros P [s H]. apply TDesc1.
    exists s. intros u. rewrite (H u), Aeq_equiv.
    split; now intros ->.
  - apply TDesc2.
Qed.

(* The quotient model inherits the description operator *)

Definition desc (P : SET' -> Prop) :=
  NS (tdelta (fun s => empred P s)).

Instance SET : ZFStruct :=
  @Build_ZFStruct SETZF' desc.

(* Hence SET satisfies extensional ZF *)

Lemma descAx (P : SET -> Prop) X :
  P X -> unique P -> P (desc P).
Proof.
  intros H1 H2.
  enough (empred P (tdelta (empred P))) by assumption.
  apply TDesc1. exists (proj1_sig X).
  intros t. split; intros H.
  - now apply NS_eq_Aeq_p1, H2.
  - symmetry in H. apply (empred_Aeq H).
    hnf. now rewrite NS_p1_eq.
Qed.

Lemma descAx1 (P : SET -> Prop) :
  iseqcl P -> P (desc P).
Proof.
  intros [X H]. apply (@descAx P X).
  - apply H. now apply set_ext.
  - intros Y Y' H1 H2.
    apply H, set_ext in H1.
    apply H, set_ext in H2.
    congruence.
Qed.

Lemma descAx2 (P P' : SET -> Prop) :
  (forall x, P x <-> P' x) -> desc P = desc P'.
Proof.
  intros H. apply Aeq_NS_eq, Aeq_ref', TDesc2.
  intros s. apply H.
Qed.

Instance SET_ZF :
  ZF SET.
Proof.
  split; try apply set_ext.
  split; try apply SETZF_ZF'.
  - apply descAx1.
  - apply descAx2.
Qed.

Hint Resolve Acz_ZF SET_ZF.

(* ACZ and SET agree on the notion of universe and strength *)

Definition ATS (s : ACZ) : SET :=
  NS s.

Lemma ATS_mor s t :
  s el t <-> ATS s el ATS t.
Proof.
  split; intros H.
  - now apply Ain_IN_NS.
  - now apply IN_Ain_NS.
Qed.

Lemma ATS_sur s x :
  x el ATS s -> exists t, t el s /\ ATS t == x.
Proof.
  intros H. exists (proj1_sig x). split.
  - now apply IN_Ain_p1_NS.
  - apply set_ext. apply NS_p1_eq.
Qed.

Fact ATS_universe u :
  universe u <-> universe (ATS u).
Proof.
  apply h_universe.
  - apply ATS_mor.
  - apply ATS_sur.
Qed.

Fact ATS_strength s n:
  strength n s <-> strength n (ATS s).
Proof.
  apply h_strength.
  - apply ATS_mor.
  - apply ATS_sur.
Qed.