Require Export Aczel.

(* Quotient construction assuming canonical representatives (CR) and proof irrelevance (PI) *)

Section CR.

Class Normalizer :=
  {
    N : Acz -> Acz;
    CR1 : forall s, Aeq s (N s);
    CR2 : forall s t, Aeq s t -> N s = N t;
    PI : forall s (H H' : N s = s), H = H';
  }.

Context { Norm : Normalizer }.

Lemma N_idem s :
  N (N s) = N s.
Proof.
  apply CR2. symmetry. apply CR1.
Qed.

Lemma N_eq_Aeq s t :
  N s = N t -> Aeq s t.
Proof.
  intros H. rewrite (CR1 s), (CR1 t). now rewrite H.
Qed.

Instance N_proper :
  Proper (Aeq ==> Aeq) N.
Proof.
  intros s t H. now rewrite <- (CR1 s), <- (CR1 t).
Qed.

Definition SET' :=
  sig (fun s => N s = s).

Definition NS s : SET' :=
  exist (fun s => N s = s) (N s) (N_idem s).

Definition IN (X Y : SET') :=
  Ain (proj1_sig X) (proj1_sig Y).

Definition Subq (X Y : SET') :=
  forall Z, IN Z X -> IN Z Y.

(* Helpful Lemmas for Automation *)

Lemma Aeq_p1_NS s :
  Aeq s (proj1_sig (NS s)).
Proof.
  exact (CR1 s).
Qed.

Lemma NS_eq_Aeq_p1 s X :
  NS s = X -> Aeq s (proj1_sig X).
Proof.
  intros <-. apply Aeq_p1_NS.
Qed.

Lemma Ain_IN_p1 X Y :
  Ain (proj1_sig X) (proj1_sig Y) -> IN X Y.
Proof.
  intros H1. unfold IN. exact H1.
Qed.

Lemma Ain_IN_NS s t :
  Ain s t -> IN (NS s) (NS t).
Proof.
  intros H1. unfold IN. now repeat rewrite <- Aeq_p1_NS.
Qed.

Lemma Ain_IN_p1_NS X s :
  Ain (proj1_sig X) s -> IN X (NS s).
Proof.
  intros H1. unfold IN. now rewrite <- Aeq_p1_NS.
Qed.

Lemma Ain_IN_NS_p1 s X :
  Ain s (proj1_sig X) -> IN (NS s) X.
Proof.
  intros H1. unfold IN. now rewrite <- Aeq_p1_NS.
Qed.

Lemma IN_Ain_p1 X Y :
  IN X Y -> Ain (proj1_sig X) (proj1_sig Y).
Proof.
  tauto.
Qed.

Lemma IN_Ain_NS s t :
  IN (NS s) (NS t) -> Ain s t.
Proof.
  unfold IN. now repeat rewrite <- Aeq_p1_NS.
Qed.

Lemma IN_Ain_p1_NS X s :
  IN X (NS s) -> Ain (proj1_sig X) s.
Proof.
  unfold IN. now rewrite <- Aeq_p1_NS.
Qed.

Lemma IN_Ain_NS_p1 s X :
  IN (NS s) X -> Ain s (proj1_sig X).
Proof.
  unfold IN. now rewrite <- Aeq_p1_NS.
Qed.

Hint Resolve Ain_IN_p1 Ain_IN_NS Ain_IN_p1_NS Ain_IN_NS_p1 IN_Ain_p1 IN_Ain_NS IN_Ain_p1_NS IN_Ain_NS_p1.

Lemma ASubq_Subq_p1 X Y :
  ASubq (proj1_sig Y) (proj1_sig X) <-> Subq Y X.
Proof.
  split; intros H Z H1.
  - apply Ain_IN_p1, H. auto.
  - apply IN_Ain_NS_p1, H. auto.
Qed.

Lemma PI_eq s t (H1 : N s = s) (H2 : N t = t) :
  s = t -> exist (fun s => N s = s) s H1 = exist (fun s => N s = s) t H2.
Proof.
  intros XY. subst t. f_equal. apply PI.
Qed.

Lemma NS_p1_eq X :
  NS (proj1_sig X) = X.
Proof.
  destruct X. simpl. now apply PI_eq.
Qed.

Lemma Aeq_p1_NS_eq X s :
  Aeq (proj1_sig X) s -> X = NS s.
Proof.
  destruct X as [t H1]. simpl. intros H2. unfold NS.
  apply PI_eq. rewrite <- H1. now apply CR2.
Qed.

Lemma Aeq_p1_eq (X Y : SET') :
  Aeq (proj1_sig X) (proj1_sig Y) -> X = Y.
Proof.
  intros H. rewrite <- (NS_p1_eq Y). now apply Aeq_p1_NS_eq.
Qed.

Lemma Aeq_NS_eq s t :
  Aeq s t -> NS s = NS t.
Proof.
  intros H % CR2.
  now apply PI_eq.
Qed.

(* We define a ZF'-structure on SET' *)

Definition Sempty :=
  NS AEmpty.

Definition Supair (X Y : SET') :=
  NS (Aupair (proj1_sig X) (proj1_sig Y)).

Definition Sunion (X : SET') :=
  NS (Aunion (proj1_sig X)).

Definition Spower (X : SET') :=
  NS (Apower (proj1_sig X)).

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

Definition Ssep (P : SET' -> Prop) (X : SET') :=
  NS (Asep (empred P) (proj1_sig X)).

Definition emfun (F : SET' -> SET') :=
  fun s => proj1_sig (F (NS s)).

Definition Srepl (F : SET' -> SET') (X : SET') :=
  NS (Arepl (emfun F) (proj1_sig X)).

Definition SETSS :=
  @Build_SetStruct SET' IN.

Definition SETZS :=
  @Build_ZStruct SETSS Sempty Supair Sunion Spower Ssep.

Definition SETZF' : ZFStruct' :=
  @Build_ZFStruct' SETZS Srepl.

(* We prove the extensional axioms of ZF for the quotient type *)

(* Extensionality *)

Lemma set_ext X Y :
  Subq X Y /\ Subq Y X <-> X = Y.
Proof.
  split; intros H; try now rewrite H. destruct H as [H1 H2].
  apply Aeq_p1_eq, Aeq_ext; now apply ASubq_Subq_p1.
Qed.

(* Foundation *)

Lemma IN_WF (X : SETZF') :
  WF X.
Proof.
  destruct X as [s NX].
  induction (Ain_AWF s) as [s _ IH].
  constructor. intros [t NY] YX.
  now apply IH.
Qed.

(* Empty *)

Lemma emptyE X :
  ~ IN X Sempty.
Proof.
  intros H % IN_Ain_p1_NS. now apply AEmptyAx in H.
Qed.

(* Unordered Pairs *)

Lemma upairAx X Y Z :
  IN Z (Supair X Y) <-> Z = X \/ Z = Y.
Proof.
  split; intros H.
  - apply IN_Ain_p1_NS, AupairAx in H as [H|H].
    + left. now apply Aeq_p1_eq.
    + right. now apply Aeq_p1_eq.
  - apply Ain_IN_p1_NS, AupairAx.
    destruct H as [-> | ->]; auto.
Qed.

(* Union *)

Lemma unionAx X Z :
  IN Z (Sunion X) <-> exists Y, IN Y X /\ IN Z Y.
Proof.
  split; intros H.
  - apply IN_Ain_p1_NS, AunionAx in H as [y[Y1 Y2]].
    exists (NS y). split; auto.
  - destruct H as [Y[Y1 Y2]].
    apply Ain_IN_p1_NS, AunionAx.
    exists (proj1_sig Y). split; auto.
Qed.

(* Power *)

Lemma powerAx X Y :
  IN Y (Spower X) <-> Subq Y X.
Proof.
  split; intros H.
  - apply IN_Ain_p1_NS, ApowerAx in H.
    now apply ASubq_Subq_p1.
  - apply Ain_IN_p1_NS, ApowerAx.
    now apply ASubq_Subq_p1.
Qed.

(* Separation *)

Fact empred_Aeq P :
  cres Aeq (empred P).
Proof.
  intros s s' H % Aeq_NS_eq. unfold empred. now rewrite H.
Qed.

Lemma sepAx P X Y :
  IN Y (Ssep P X) <-> IN Y X /\ P Y.
Proof with try apply empred_Aeq.
  split; intros H.
  - apply IN_Ain_p1_NS, AsepAx in H as [H1 H2]...
    split; auto. unfold empred in H2.
    now rewrite NS_p1_eq in H2.
  - destruct H as [H1 H2]. apply Ain_IN_p1_NS, AsepAx...
    split; trivial. unfold empred. now rewrite NS_p1_eq.
Qed.

(* Functional Replacement *)

Fact emfun_Aeq F :
  fres Aeq (emfun F).
Proof.
  intros s s' H % Aeq_NS_eq.
  unfold emfun. now rewrite H.
Qed.

Lemma replAx F X Y :
  IN Y (Srepl F X) <-> exists Z, IN Z X /\ Y = F Z.
Proof with try apply emfun_Aeq.
  split; intros H.
  - apply IN_Ain_p1_NS, AreplAx in H as [z[Z1 Z2]]...
    exists (NS z). split; auto. now apply Aeq_p1_eq.
  - destruct H as [Z[Z1 Z2]].
    apply Ain_IN_p1_NS, AreplAx...
    exists (proj1_sig Z). split; auto.
    rewrite Z2. unfold emfun.
    now rewrite NS_p1_eq.
Qed.

(* The main result is that SETZF satisfies extensional ZF' *)

Lemma SETZF_Z :
  iZ SETZF'.
Proof.
  split; try apply IN_WF. split.
  - now intros X X' Y -> % set_ext.
  - apply emptyE.
  - intros X Y Z. unfold equiv.
    do 2 rewrite set_ext. apply upairAx.
  - apply unionAx.
  - apply powerAx.
  - intros P X Y _. apply sepAx.
Qed.

Theorem SETZF_ZF' :
  ZF' SETZF'.
Proof.
  split; try apply set_ext.
  split; try apply SETZF_Z.
  intros F X Z _. rewrite replAx.
  split; intros [Y[Y1 Y2]]; exists Y.
  - now rewrite <- set_ext in Y2.
  - now rewrite <- set_ext.
Qed.

Lemma NS_powit n :
  proj1_sig (@powit SETZF' n) == (@powit ACZ' n).
Proof.
  induction n; simpl; apply Aeq_equiv.
  - now rewrite <- CR1.
  - apply Aeq_equiv in IHn.
    now rewrite IHn, <- CR1.
Qed.

Fact SETZF_Inf :
  Inf SETZF'.
Proof.
  exists (NS Aom). intros x. split; intros H.
  - apply IN_Ain_p1_NS, Aom_spec in H as [n H].
    exists n. rewrite <- NS_powit, Aeq_equiv in H.
    apply (@ZFExt' SETZF' SETZF_ZF').
    now apply Aeq_p1_eq.
  - destruct H as [n H].
    apply (@ZFExt' SETZF' SETZF_ZF') in H as ->.
    apply Ain_IN_p1_NS, Aom_spec. exists n.
    now apply NS_powit.
Qed.

End CR.

Hint Resolve Ain_IN_p1 Ain_IN_NS Ain_IN_p1_NS Ain_IN_NS_p1 IN_Ain_p1 IN_Ain_NS IN_Ain_p1_NS IN_Ain_NS_p1.