Require Export Aczel.

(* Quotient construction assuming class extensionality (CE) and proof irrelevance (PI) *)

Definition eqclass P :=
  exists s, P = Aeq s.

Axiom CE : forall (P Q : Acz -> Prop), (forall s, P s <-> Q s) -> P = Q.
Axiom PI : forall P (H H' : eqclass P), H = H'.

Definition SET' :=
  { P | eqclass P }.

Definition class (X : SET') : Acz -> Prop :=
  proj1_sig X.

Definition ele X Y :=
  forall s t, (class X) s -> (class Y) t -> Ain s t.

Definition sub X Y :=
  forall Z, ele Z X -> ele Z Y.

Lemma Aeq_eqclass s :
  eqclass (Aeq s).
Proof.
  now exists s.
Qed.

Hint Resolve Aeq_eqclass.

(* Facts about equivalence classes *)

Definition classof (s : Acz) : SET' :=
  exist _ (Aeq s) (Aeq_eqclass s).

Lemma class_eq X X' s s' :
  Aeq s s' -> class X s -> class X' s' -> X = X'.
Proof.
  destruct X as [P HP], X' as [P' HP']; simpl.
  intros H1 H2 XX. assert (H : P = P').
  - destruct HP as [t ->], HP' as [t' ->].
    apply CE. intros u. rewrite H2, H1, XX. tauto.
  - subst P'. now rewrite (PI HP HP').
Qed.

Lemma classof_ex X :
  exists s, X = classof s.
Proof.
  destruct X as [P[s ->]]; simpl. exists s.
  apply (class_eq (s:=s) (s':=s)); simpl; auto.
Qed.

Lemma classof_class s :
  class (classof s) s.
Proof.
  simpl. reflexivity.
Qed.

Lemma classof_eq s t :
  classof s = classof t <-> Aeq s t.
Proof.
  split; intros H.
  - specialize (classof_class s).
    intros XX. rewrite H in XX. auto.
  - apply (class_eq H); simpl; trivial.
Qed.

Lemma classof_ele s t :
  ele (classof s) (classof t) <-> Ain s t.
Proof.
  split; intros H.
  - apply H; simpl; auto.
  - intros s' t' H1 H2. now rewrite <- H1, <- H2.
Qed.

Lemma classof_sub s t :
  sub (classof s) (classof t) <-> ASubq s t.
Proof.
  split; intros H1.
  - intros u H2. now apply classof_ele, H1, classof_ele.
  - intros Z H2. destruct (classof_ex Z) as [u ->].
    now apply classof_ele, H1, classof_ele.
Qed.

Hint Resolve classof_class classof_eq classof_ele classof_sub.

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

Definition empty :=
  classof AEmpty.

Definition upair' X Y u :=
  exists s t, (class X) s /\ (class Y) t /\ Aeq u (Aupair s t).

Lemma upair_eqclass X Y :
  eqclass (upair' X Y).
Proof.
  destruct (classof_ex X) as [s ->].
  destruct (classof_ex Y) as [t ->].
  exists (Aupair s t). apply CE. intros z. split; intros H.
  - destruct H as [s'[t'[H1[H2 H3]]]]; simpl in H1, H2.
    now rewrite H1, H2, H3.
  - exists s, t. simpl. repeat split; auto.
Qed.

Definition upair X Y :=
  exist _ (upair' X Y) (upair_eqclass X Y).

Definition union' X t :=
  exists s, (class X) s /\ Aeq t (Aunion s).

Lemma union_eqclass X :
  eqclass (union' X).
Proof.
  destruct (classof_ex X) as [s ->].
  exists (Aunion s). apply CE. intros z. split; intros H.
  - destruct H as [s'[H1 H2]]; simpl in H1.
    now rewrite H1, H2.
  - exists s. auto.
Qed.

Definition union X :=
  exist _ (union' X) (union_eqclass X).

Definition power' X t :=
  exists s, (class X) s /\ Aeq t (Apower s).

Lemma power_eqclass X :
  eqclass (power' X).
Proof.
  destruct (classof_ex X) as [s ->].
  exists (Apower s). apply CE. intros t. split; intros H.
  - destruct H as [s'[H1 H2]]; simpl in H1.
    now rewrite H1, H2.
  - exists s. auto.
Qed.

Definition power X :=
  exist _ (power' X) (power_eqclass X).

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

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

Definition sep' P X t :=
  exists s, (class X) s /\ Aeq t (Asep (empred P) s).

Lemma sep_eqclass P X :
  eqclass (sep' P X).
Proof.
  destruct (classof_ex X) as [s ->].
  exists (Asep (empred P) s). apply CE. intros t. split; intros H.
  - destruct H as [s'[H1 H2]]; simpl in H1.
    now rewrite H2, (Asep_proper (@empred_Aeq P) H1).
  - exists s. auto.
Qed.

Definition sep P X :=
  exist _ (sep' P X) (sep_eqclass P X).

Definition SETSS :=
  @Build_SetStruct SET' ele.

Instance SET : ZStruct :=
  @Build_ZStruct SETSS empty upair union power sep.

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

(* Extensionality *)

Lemma set_ext X Y :
  sub X Y /\ sub Y X <-> X = Y.
Proof.
  destruct (classof_ex X) as [s ->].
  destruct (classof_ex Y) as [t ->].
  repeat rewrite classof_sub. rewrite classof_eq.
  apply Aeq_equiv.
Qed.

(* Foundation *)

Lemma ele_WF (X : SET) :
  WF X.
Proof.
  destruct (classof_ex X) as [s ->].
  induction (Ain_AWF s) as [s _ IH].
  constructor. intros Y H.
  destruct (classof_ex Y) as [t ->].
  now apply IH, classof_ele.
Qed.

(* Empty *)

Lemma emptyE X :
  ~ ele X empty.
Proof.
  destruct (classof_ex X) as [s ->].
  unfold empty. rewrite classof_ele.
  apply AEmptyAx.
Qed.

(* Unordered Pairs *)

Lemma upair_welldef s t :
  upair (classof s) (classof t) = classof (Aupair s t).
Proof.
  pose (u := Aupair s t).
  apply (class_eq (s:=u) (s':=u)); trivial.
  exists s, t. auto.
Qed.

Lemma upairAx X Y Z :
  ele Z (upair X Y) <-> Z = X \/ Z = Y.
Proof.
  destruct (classof_ex Z) as [u ->].
  destruct (classof_ex X) as [s ->].
  destruct (classof_ex Y) as [t ->].
  repeat rewrite classof_eq.
  rewrite upair_welldef, classof_ele.
  apply AupairAx.
Qed.

(* Union *)

Lemma union_welldef s :
  union (classof s) = classof (Aunion s).
Proof.
  pose (t := Aunion s).
  apply (class_eq (s:=t) (s':=t)); trivial.
  exists s. auto.
Qed.

Lemma unionAx X Z :
  ele Z (union X) <-> exists Y, ele Y X /\ ele Z Y.
Proof.
  destruct (classof_ex Z) as [u ->].
  destruct (classof_ex X) as [s ->].
  rewrite union_welldef, classof_ele, AunionAx.
  split; intros [t H].
  - exists (classof t). now repeat rewrite classof_ele.
  - destruct (classof_ex t) as [t' ->].
    exists t'. now repeat rewrite <- classof_ele.
Qed.

(* Power *)

Lemma power_welldef s :
  power (classof s) = classof (Apower s).
Proof.
  pose (t := Apower s).
  apply (class_eq (s:=t) (s':=t)); trivial.
  exists s. auto.
Qed.

Lemma powerAx X Y :
  ele Y (power X) <-> sub Y X.
Proof.
  destruct (classof_ex Y) as [t ->].
  destruct (classof_ex X) as [s ->].
  rewrite power_welldef, classof_ele, classof_sub.
  apply ApowerAx.
Qed.

(* Separation *)

Lemma sep_welldef P s :
  sep P (classof s) = classof (Asep (empred P) s).
Proof.
  pose (t := Asep (empred P) s).
  apply (class_eq (s:=t) (s':=t)); trivial.
  exists s. auto.
Qed.

Lemma sepAx P X Y :
  ele Y (sep P X) <-> ele Y X /\ P Y.
Proof.
  destruct (classof_ex Y) as [s ->].
  destruct (classof_ex X) as [t ->].
  rewrite sep_welldef. repeat rewrite classof_ele.
  apply AsepAx, empred_Aeq.
Qed.

(* The main result is that SET satisfies Z with infinity *)

Instance SET_Z :
  Z SET.
Proof.
  split; try apply set_ext.
  split; try apply ele_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.

Lemma classof_powit n :
  classof (@powit ACZ' n) = (@powit SET n).
Proof.
  induction n; simpl.
  - reflexivity.
  - now rewrite <- power_welldef, <- IHn.
Qed.

Fact SET_Inf :
  Inf SET.
Proof.
  exists (classof Aom). intros X.
  destruct (classof_ex X) as [s ->].
  rewrite classof_ele, (Aom_spec s).
  split; intros [n H]; exists n.
  - rewrite <- classof_powit, ZExt.
    now apply classof_eq, Aeq_equiv.
  - rewrite <- classof_powit, ZExt in H.
    now apply Aeq_equiv, classof_eq.
Qed.