# Extensional Model of Z via Class Extensionality

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.