# Membership Embeddings

Require Export Prelims.

(* We assume a memberhip-morphism h between models M N and show that h respects universes *)

Section Mor.

Context { M : ZFStruct }.
Context { M_iZF : iZF M }.

Context { N : ZFStruct' }.
Context { N_iZF : iZF' N }.

Variable h : M -> N.
Hypothesis h_mor : forall x y, x el y <-> h x el h y.
Hypothesis h_sur : forall x y', y' el h x -> exists y, y el x /\ h y == y'.

(* h respects inclusion, equivalence, transitivity and swelledness *)

Lemma h_sub x y :
x <<= y <-> h x <<= h y.
Proof.
split; intros H.
- intros z' [z [Z <-]] % h_sur. now apply h_mor, H.
- intros z Z. now apply h_mor, H, h_mor.
Qed.

Lemma h_equiv x y :
x == y <-> h x == h y.
Proof.
unfold equiv. repeat rewrite h_sub. tauto.
Qed.

Global Instance h_Proper :
Proper (equiv ==> equiv) h.
Proof.
intros x y. apply h_equiv.
Qed.

Lemma h_cres x' :
cres equiv (fun y => h y el x').
Proof.
intros y y' Y % h_equiv. now rewrite Y.
Qed.

Lemma h_sur_sub x y' :
y' <<= h x -> exists y, y <<= x /\ h y == y'.
Proof with eauto using h_cres.
intros H. pose (y := sep (fun z => h z el y') x). exists y. split.
- intros z [Z1 Z2] % Sep...
- split; intros z' Z.
+ apply h_sur in Z as [z[Z1 <-]].
apply Sep in Z1 as []...
+ destruct (h_sur (H z' Z)) as [z[Z1 Z2]].
rewrite <- Z2. apply h_mor.
apply Sep... rewrite Z2. split; assumption.
Qed.

Lemma h_trans1 x :
trans x -> trans (h x).
Proof.
intros H y' z' [y [Y <-]] % h_sur [z [Z <-]] % h_sur.
apply h_mor. now apply (H y).
Qed.

Lemma h_trans2 x :
trans (h x) -> trans x.
Proof.
intros H y Y z Z. apply h_mor, (H (h y)); now apply h_mor.
Qed.

Lemma h_swelled1 x :
swelled x -> swelled (h x).
Proof.
intros H y' z' [y [Y <-]] % h_sur [z [Z <-]] % h_sur_sub.
now apply h_mor, (H y).
Qed.

Lemma h_swelled2 x :
swelled (h x) -> swelled x.
Proof.
intros H y z. repeat rewrite h_mor.
rewrite h_sub. apply H.
Qed.

(* h resepects the operations of Z *)

Lemma h_eset :
h 0 == 0.
Proof.
split; intros x; intros H; auto.
destruct (h_sur H) as [y [Y _]]; auto.
Qed.

Lemma h_upair x y :
h (upair x y) == upair (h x) (h y).
Proof.
split; intros z' Z.
- apply h_sur in Z as [z [Z <-]]. apply Pair.
repeat rewrite <- h_equiv. now apply Pair.
- apply Pair in Z as [-> | ->]; apply h_mor, Pair.
+ left. reflexivity.
+ right. reflexivity.
Qed.

Lemma h_union x :
h (union x) == union (h x).
Proof.
split; intros z' Z.
- apply h_sur in Z as [z [Z <-]].
apply Union in Z as [y Y].
apply Union. exists (h y). now repeat rewrite <- h_mor.
- apply Union in Z as [y'[Y1 Y2]].
apply h_sur in Y1 as [y [Y Y']]. rewrite <- Y' in Y2.
apply h_sur in Y2 as [z [Z <-]].
apply h_mor, Union. now exists y.
Qed.

Lemma h_power x :
h (power x) == power (h x).
Proof.
split; intros y' Y.
- apply h_sur in Y as [y [Y <-]].
now apply Power, h_sub, Power.
- apply Power, h_sur_sub in Y as [y[Y <-]].
now apply h_mor, Power.
Qed.

(* h respects functional replacement *)

Definition preim x' :=
delta (fun x => h x == x').

Lemma delta_equiv P x :
iseqcl P -> x == delta P <-> P x.
Proof.
intros H1. assert (H2 : P (delta P)) by now apply Desc1.
destruct H1 as [x' H1]. split; intros H.
- apply H1. rewrite H. now apply H1.
- apply H1 in H2 as ->. now apply H1.
Qed.

Lemma preim_equiv x x' :
h x == x' -> x == preim x'.
Proof.
intros H. apply delta_equiv; trivial.
exists x. intros y. now rewrite <- H, h_equiv.
Qed.

Lemma preim_equiv' x' :
(exists x, h x == x') -> x' == h (preim x').
Proof.
intros [x X]. rewrite <- X at 1.
now apply h_equiv, preim_equiv.
Qed.

Definition NTM F x :=
preim (F (h x)).

Lemma NTM_fres F :
fres equiv F -> fres equiv (NTM F).
Proof.
intros FR x x' H % h_equiv.
apply eq_equiv, Desc2. unfold iseqcl.
intros y. now rewrite (FR (h x) (h x') H).
Qed.

Lemma h_frep1 F x x' :
fres equiv F -> (forall z', z' el frep F x' -> exists z, h z == z')
-> h x == x' -> h (frep (NTM F) x) == frep F x'.
Proof with eauto using NTM_fres.
intros FR FS X. split; intros z' Z'.
- destruct (h_sur Z') as [z[Z1 Z2]].
rewrite <- Z2. apply Frep...
apply Frep in Z1 as [y[Y1 Y2]]...
exists (h y). rewrite <- X, <- h_mor. split; trivial.
rewrite Y2. symmetry. apply preim_equiv', FS, Frep...
exists (h y). rewrite <- X, <- h_mor.
split; trivial. reflexivity.
- destruct (FS z' Z') as [z Z].
rewrite <- Z. apply h_mor. apply Frep...
apply Frep in Z' as [y'[Y1' Y2']]...
rewrite <- X in Y1'. destruct (h_sur Y1') as [y[Y1 Y2]].
exists y. split; trivial. apply preim_equiv.
rewrite Z, Y2'. now apply FR.
Qed.

Definition MTN F x' :=
h (F (preim x')).

Definition MTN_fres F :
fres equiv F -> fres equiv (MTN F).
Proof.
intros FR x x' H. apply h_equiv, FR.
apply eq_equiv. apply Desc2.
intros y. now rewrite H.
Qed.

Lemma h_frep2 F x :
fres equiv F -> h (frep F x) == frep (MTN F) (h x).
Proof with eauto using MTN_fres.
intros FR. split; intros z' Z'.
- destruct (h_sur Z') as [z[Z <-]].
apply Frep in Z as [y[Y ->]]...
apply Frep... exists (h y). rewrite <- h_mor.
split; trivial. apply h_equiv.
apply FR. now apply preim_equiv.
- apply Frep in Z' as [y'[Y ->]]...
apply h_sur in Y as [y[Y1 Y2]].
apply h_mor. apply Frep...
exists y. split; trivial. apply FR.
symmetry. now apply preim_equiv.
Qed.

(* h respects ZF-closed classes *)

Definition img P :=
fun x' => exists x, h x == x' /\ P x.

Lemma img_agree x :
agree (img (cl x)) (h x).
Proof.
intros y'. split.
- intros [y[Y1 Y2]] % h_sur. now exists y.
- intros [y[<- Y]]. now apply h_mor.
Qed.

Instance img_Proper P :
Proper (equiv ==> iff) (img P).
Proof.
intros x y H. split; intros [a[A1 A2]].
- exists a. split; trivial. now rewrite A1.
- exists a. split; trivial. now rewrite A1.
Qed.

Lemma img_P (P : M -> Prop) x :
P x -> img P (h x).
Proof.
intros H. exists x. split; trivial. reflexivity.
Qed.

Lemma img_cres P :
cres equiv (img P).
Proof.
intros x' y' H [x[X1 X2]].
exists x. rewrite X1. split; assumption.
Qed.

Hint Resolve img_P img_cres.

Lemma img_ctrans1 P :
ctrans P -> ctrans (img P).
Proof.
intros H x' y' [x[X1 X2]] X.
rewrite <- X1 in X. apply h_sur in X as [y[Y1 Y2]].
exists y. split; trivial. now apply (H x).
Qed.

Lemma img_ctrans2 P :
cres equiv P -> ctrans (img P) -> ctrans P.
Proof.
intros PR H x y X1 X2 % h_mor.
destruct (H (h x) (h y)) as [z Z]; auto.
rewrite <- h_equiv in Z.
apply (PR z y); apply Z.
Qed.

Lemma img_cswelled1 P :
cswelled P -> cswelled (img P).
Proof.
intros H x' y' [x[<- X1]] X2.
apply h_sur_sub in X2 as [y[Y1 Y2]].
exists y. split; trivial. now apply (H x y).
Qed.

Lemma img_cswelled2 P :
cres equiv P -> cswelled (img P) -> cswelled P.
Proof.
intros PR H x y X1 X2 % h_sub.
destruct (H (h x) (h y)) as [z[Z1 Z2]]; auto.
apply h_equiv in Z1. now apply (PR z).
Qed.

Lemma img_Z1 P :
cres equiv P -> closed_Z P -> closed_Z (img P).
Proof.
intros PR H. split.
- apply img_ctrans1, H.
- exists 0. split; [apply h_eset | apply H].
- intros x' y' [x[<- X]] [y[<- Y]].
rewrite <- h_upair. now apply img_P, H.
- intros x' [x[<- X]]. rewrite <- h_union.
now apply img_P, H.
- intros x' [x[<- X]]. rewrite <- h_power.
now apply img_P, H.
- now apply cswelled_sep, img_cswelled1, sep_cswelled, H.
Qed.

Lemma img_Z2 P :
cres equiv P -> closed_Z (img P) -> closed_Z P.
Proof.
intros PR []. split.
- now apply img_ctrans2, U_trans.
- destruct U_eset as [x[X1 X2]]. apply (PR x); trivial.
rewrite h_equiv, X1, h_eset. reflexivity.
- intros x y H1 H2. destruct (U_upair (h x) (h y)) as [z[Z1 Z2]]; auto.
rewrite <- h_upair, <- h_equiv in Z1. now apply (PR z).
- intros x H. destruct (U_union (h x)) as [z[Z1 Z2]]; auto.
rewrite <- h_union, <- h_equiv in Z1. now apply (PR z).
- intros x H. destruct (U_power (h x)) as [z[Z1 Z2]]; auto.
rewrite <- h_power, <- h_equiv in Z1. now apply (PR z).
- now apply cswelled_sep, img_cswelled2, sep_cswelled, U_sep.
Qed.

Lemma img_frep1 P :
cres equiv P -> closed_frep P -> closed_frep (img P).
Proof.
intros PR H F x' FR [x[X1 X2]] FS.
assert (X : h (frep (NTM F) x) == frep F x').
- apply h_frep1; trivial.
intros z' Z. apply FS in Z as [z Z]. now exists z.
- exists (frep (NTM F) x). split; trivial.
apply H; eauto using NTM_fres.
intros z Z % h_mor. rewrite X in Z.
apply FS in Z as [y[Y1 % h_equiv Y2]]. now apply (PR y).
Qed.

Lemma img_frep2 P :
cres equiv P -> closed_frep (img P) -> closed_frep P.
Proof.
intros PR H F x FR HX FS.
assert (X : h (frep F x) == frep (MTN F) (h x)).
- now apply h_frep2.
- cut (img P (h (frep F x))).
+ intros [y[Y1 % h_equiv Y2]]. now apply (PR y).
+ rewrite X. apply H; eauto using MTN_fres.
intros z'. rewrite <- X. intros [z[Z1 Z2]] % h_sur.
exists z. split; trivial. now apply FS.
Qed.

Lemma img_ZF P :
cres equiv P -> closed_ZF P <-> closed_ZF (img P).
Proof.
intros PR. split; intros H; split.
- now apply img_Z1, H.
- now apply img_frep1, H.
- now apply img_Z2, H.
- now apply img_frep2, H.
Qed.

(* Main results: h respects universes and strength *)

Theorem h_universe u :
universe u <-> universe (h u).
Proof.
unfold universe. rewrite img_ZF; try apply cres_cl.
apply ZF_proper. intros x'. split; intros H.
- destruct H as [x[<- X]]. now apply h_mor.
- apply h_sur in H as [x[X <-]]. auto.
Qed.

Lemma h_const P :
cequiv P (img const) -> closed_ZF P.
Proof.
intros ->. apply img_ZF; firstorder.
Qed.

Theorem h_strength n x :
strength n x <-> strength n (h x).
Proof.
revert x. induction n; simpl; try tauto.
intros x. split; intros [u[U1[U2 U3]]].
- exists (h u). now rewrite <- h_mor, <- h_universe, <- IHn.
- apply h_sur in U1 as [u'[U1' U2']].
exists u'. now rewrite h_universe, IHn, U2'.
Qed.

End Mor.