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.