# Extensional Model of ZF' via Canonical Representatives

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.