Require Export Stage.

(* Definition of Iso, the model similarity *)

Definition btot (M N : SetStruct) (R : M -> N -> Prop) x a :=
  forall y, y el x -> exists b, b el a /\ R y b.

Definition bsur (M N : SetStruct) (R : M -> N -> Prop) x a :=
  forall b, b el a -> exists y, y el x /\ R y b.

Inductive Iso (M N : SetStruct) (x : M) (a : N) : Prop :=
| II : btot Iso x a -> bsur Iso x a -> Iso x a.

(* Iso is symmetric *)

Lemma Iso_sym (M N : SetStruct) (MZF : ZF M) (x : M) (a : N) :
  Iso x a -> Iso a x.
Proof.
  assert (H : WF x) by apply MZF.
  revert a. induction H as [x _ IHx].
  intros a [H1 H2]. split.
  - intros b B. destruct (H2 b B) as [y[Y1 Y2]].
    exists y. split; trivial. apply IHx; trivial.
  - intros y Y. destruct (H1 y Y) as [b[B1 B2]].
    exists b. split; trivial. apply IHx; trivial.
Qed.

Lemma btot_bsur (M N : SetStruct) {MZF : ZF M} {NZF : ZF N} (x : M) (a : N) :
  btot (@Iso M N) x a <-> bsur (@Iso N M) a x.
Proof.
  split.
  - intros H y Y. destruct (H y Y) as [b[B1 B2]].
    exists b. split; trivial. now apply Iso_sym.
  - intros H y Y. destruct (H y Y) as [b[B1 B2]].
    exists b. split; trivial. now apply Iso_sym.
Qed.

(* Iso is functional and respects membership *)

Section Iso.

Context { M : SetStruct }.
Context { MZF : ZF M }.

Context { N : SetStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Definition domain x :=
  exists a, Iso x a.

Definition range a :=
  exists x, Iso x a.

Fact tot_sur :
   surjective (@Iso N M) <-> total (@Iso M N).
Proof.
  split; intros H x; destruct (H x) as [a I % Iso_sym]; eauto.
Qed.

Fact Iso_btot x a :
  Iso x a -> btot (@Iso M N) x a.
Proof.
  now intros [].
Qed.

Fact Iso_bsur x a :
  Iso x a -> bsur (@Iso M N) x a.
Proof.
  now intros [].
Qed.

Lemma Iso_fun :
  functional (@Iso M N).
Proof.
  intros x.
  induction (AxWF x) as [x _ IH].
  intros a b [H1 H2] [I1 I2].
  apply Ext; intros c C.
  - destruct (H2 c C) as [y [Y1 Y2]].
    destruct (I1 y Y1) as [d [D1 D2]].
    rewrite (IH y Y1 c d); eauto.
  - destruct (I2 c C) as [y [Y1 Y2]].
    destruct (H1 y Y1) as [d [D1 D2]].
    rewrite (IH y Y1 c d); eauto.
Qed.

Lemma Iso_res x y a b :
  Iso x a -> Iso y b -> y el x -> b el a.
Proof.
  intros [X _] Y H.
  destruct (X y H) as [b'[B1 B2]].
  now rewrite (Iso_fun Y B2).
Qed.

End Iso.

(* Iso respects the other set constructors *)

Section Cons.

Context { M : SetStruct }.
Context { MZF : ZF M }.

Context { N : SetStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Fact Iso_inj :
  injective (@Iso M N).
Proof.
  intros x y a X % Iso_sym Y % Iso_sym; trivial.
  apply (Iso_fun X Y).
Qed.

Fact Iso_mem x y a b :
  Iso x a -> Iso y b -> (y el x <-> b el a).
Proof.
  intros X Y. split; intros H.
  - now apply (Iso_res X Y).
  - now apply (Iso_res (Iso_sym MZF X) (Iso_sym MZF Y)).
Qed.

Lemma btot_eset :
  btot (@Iso M N) 0 0.
Proof.
  intros x H. auto.
Qed.

Lemma btot_union x a :
  btot (@Iso M N) x a -> btot (@Iso M N) (union x) (union a).
Proof.
  intros H y [z[Z1 Z2]] % Union.
  destruct (H z Z1) as [c[C1 [C2 _]]].
  destruct (C2 y Z2) as [b[B1 B2]].
  exists b. split; trivial. apply Union. now exists c.
Qed.

Lemma btot_power x a :
  btot (@Iso M N) x a -> btot (@Iso M N) (power x) (power a).
Proof.
  intros H y Y % Power.
  pose (b := a ! (fun c => exists z, z el y /\ Iso z c)).
  exists b. split; try apply Power, sep_sub. split.
  - intros z Z. destruct (H z (Y z Z)) as [c [C1 C2]].
    exists c. split; trivial. apply sep_el. split; eauto.
  - intros c C. now apply sep_el in C as [].
Qed.

Definition MtoN (R : M -> M -> Prop) a b :=
  exists x y, Iso x a /\ Iso y b /\ R x y.

Fact MtoN_fun R :
  functional R -> functional (MtoN R).
Proof.
  intros H a b c (x&y&I1&I2&I3) (x'&z&J1&J2&J3).
  rewrite (Iso_inj J1 I1) in J3.
  rewrite (H x y z I3 J3) in I2.
  apply (Iso_fun I2 J2).
Qed.

Lemma btot_rep R x a :
  functional R -> (rep R x) <=c domain ->
  btot (@Iso M N) x a -> btot (@Iso M N) (rep R x) (rep (MtoN R) a).
Proof with eauto using MtoN_fun.
  intros FR XD H y Y. destruct (XD y Y) as [b B].
  exists b. split; trivial. apply Rep...
  apply Rep in Y as [z[Z1 Z2]]...
  destruct (H z Z1) as [c[C1 C2]].
  exists c. split; trivial. now exists z, y.
Qed.

Fact bsur_rep R x a :
  functional R -> (rep R x) <=c domain ->
  Iso x a -> bsur (@Iso M N) (rep R x) (rep (MtoN R) a).
Proof with eauto using MtoN_fun.
  intros FR XD H b B. apply Rep in B as [c[C[z[y[Z[Y I]]]]]]...
  exists y. split; trivial. apply Rep... exists z. split; trivial.
  now apply (Iso_mem H Z).
Qed.

End Cons.

(* The domain forms a universe *)

Section Domain.

Context { M : SetStruct }.
Context { MZF : ZF M }.

Context { N : SetStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Lemma Iso_eset :
  (@Iso M N) 0 0.
Proof.
  split.
  - apply btot_eset.
  - now apply btot_bsur, btot_eset.
Qed.

Lemma Iso_union x a :
  Iso x a -> Iso (union x) (union a).
Proof.
  intros [H I]. split.
  - now apply btot_union.
  - now apply btot_bsur, btot_union, btot_bsur.
Qed.

Lemma Iso_power x a :
  Iso x a -> Iso (power x) (power a).
Proof.
  intros [H I]. split.
  - now apply btot_power.
  - now apply btot_bsur, btot_power, btot_bsur.
Qed.

Lemma Iso_rep R x a :
  functional R -> (rep R x) <=c domain ->
  Iso x a -> Iso (rep R x) (rep (MtoN R) a).
Proof.
  intros FR XD H. split.
  - now apply btot_rep, H.
  - now apply bsur_rep.
Qed.

Fact Iso_dom x a :
  Iso x a -> (@domain M N) x.
Proof.
  intros H. now exists a.
Qed.

Fact Iso_dom' x a :
  Iso x a -> (@domain N M) a.
Proof.
  intros H % Iso_sym; trivial. unfold domain. now exists x.
Qed.

Fact domain_union x :
  domain x -> domain (union x).
Proof.
  intros [a H % Iso_union]. now exists (union a).
Qed.

Fact domain_power x :
  domain x -> domain (power x).
Proof.
  intros [a H % Iso_power]. now exists (power a).
Qed.

Fact domain_rep R x :
  functional R -> (rep R x) <=c domain ->
  domain x -> domain (rep R x).
Proof.
  intros FR XD [a H % (Iso_rep FR XD)]. eapply Iso_dom, H.
Qed.

Fact domain_el x y :
  domain x -> y el x -> domain y.
Proof.
  intros [a H] I. destruct (Iso_btot H I) as [b [_ J]]. now exists b.
Qed.

Fact domain_sub x y :
  domain x -> y <<= x -> domain y.
Proof.
  intros [a H % Iso_power] I % Power.
  destruct (Iso_btot H I) as [b [_ J]]. now exists b.
Qed.

Fact union_domain x :
  domain (union x) -> domain x.
Proof.
  intros [b H % Iso_power % Iso_power].
  assert (I : x el (power (power (union x)))).
  - apply Power. intros y I. apply Power. now apply union_el_sub.
  - destruct (Iso_btot H I) as [a [_ J]]. now exists a.
Qed.

Lemma domain_universe :
  agree (@domain M N) <=p universe.
Proof.
  intros u H. repeat split.
  - intros x X % H y Y. apply H. now apply (domain_el X Y).
  - apply H. exists 0. apply Iso_eset.
  - intros x X % H. apply H. now apply domain_union.
  - intros x X % H. apply H. now apply domain_power.
  - intros R x FR XD X % H. apply H. apply domain_rep; trivial.
    intros y [z [Z1 Z2]] % Rep; trivial. now apply H, (XD z).
Qed.

Lemma Iso_Stage x a :
  Iso x a -> Stage x -> Stage a.
Proof.
  intros H I. revert a H. induction I as [x I IH | x I IH].
  - intros b H. destruct (Iso_btot H (power_eager x)) as [a [A1 A2]].
    specialize (IH a A2). apply Iso_power in A2.
    rewrite <- (Iso_fun A2); auto. now constructor.
  - intros b H. destruct (union_domain (Iso_dom H)) as [a J].
    rewrite (Iso_fun H (Iso_union J)). constructor. intros c C.
    destruct (Iso_bsur J C) as [y [Y1 Y2]]. now apply (IH y).
Qed.

End Domain.

(* Iso respects universes *)

Section Universes.

Context { M : SetStruct }.
Context { MZF : ZF M }.

Context { N : SetStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Fact Iso_trans x a :
  Iso x a -> trans x -> trans a.
Proof.
  intros H1 H2 b B c C.
  destruct (Iso_bsur H1 B) as [y[Y1 Y2]].
  destruct (Iso_bsur Y2 C) as [z[Z1 Z2]].
  apply (Iso_mem H1 Z2). now apply H2 with (y:=y).
Qed.

Fact Iso_closed_union x a :
  Iso x a -> closed_union x -> closed_union a.
Proof.
  intros H1 H2 b B. destruct (Iso_bsur H1 B) as [y[Y1 Y2]].
  apply Iso_union in Y2. now apply (Iso_mem H1 Y2), H2.
Qed.

Fact Iso_closed_power x a :
  Iso x a -> closed_power x -> closed_power a.
Proof.
  intros H1 H2 b B. destruct (Iso_bsur H1 B) as [y[Y1 Y2]].
  apply Iso_power in Y2. now apply (Iso_mem H1 Y2), H2.
Qed.

Fact Iso_closed_rep x a :
  Iso x a -> closed_rep x -> closed_rep a.
Proof.
  intros H1 H2 R b H3 H4 B. destruct (Iso_bsur H1 B) as [y[Y1 Y2]].
  apply Iso_sym, (Iso_rep H3) in Y2 as Y3; trivial.
  - apply Iso_sym in H1; trivial.
    apply (Iso_mem H1 Y3), H2; trivial.
    + now apply MtoN_fun.
    + intros z z' [c[c'[Z1[Z2 Z3]]]] Z. apply (Iso_mem H1 Z2).
      apply (H4 c); trivial. now apply (Iso_mem Y2 Z1).
  - intros c [d[D1 D2]] % Rep; trivial.
    apply (domain_el (x:=a)); trivial.
    + exists x. now apply Iso_sym.
    + now apply (H4 d).
Qed.

Lemma Iso_universe x a :
  Iso x a -> universe x -> universe a.
Proof.
  intros H1 H2. repeat split.
  - apply (Iso_trans H1), H2.
  - apply (Iso_mem H1 Iso_eset). apply H2.
  - apply (Iso_closed_union H1), H2.
  - apply (Iso_closed_power H1), H2.
  - apply (Iso_closed_rep H1), H2.
Qed.

End Universes.

(* Facts about stages *)

Section Stages.

Context { M : SetStruct }.
Context { MZF : ZF M }.

Context { N : SetStruct }.
Context { NZF : ZF N }.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Fact Stage_btot x a :
  least (fun x' => Stage x' /\ ~ domain x') x -> Stage a -> ~ (@domain N M) a -> btot (@Iso M N) x a.
Proof.
  intros [[XS XD] XL] AS AR.
  induction XS as [x H IH | x H IH].
  - exfalso. destruct (classic (domain x)).
    + now apply XD, domain_power.
    + now apply (power_above (x:=x)), XL.
  - destruct (Stage_dicho H) as [I|I]; try now apply IH.
    intros y Y. apply Union in Y as [z [Z1 Z2]].
    destruct (classic (domain z)) as [[c C]|J].
    + assert (CS : Stage c) by exact (Iso_Stage C (H z Z1)).
      destruct (Stage_lin_el AS CS) as [J|J].
      * exfalso. apply AR. apply (domain_sub (Iso_dom' C) J).
      * destruct (Iso_btot C Z2) as [b [B1 B2]].
        exists b. split; trivial. now apply (Stage_trans AS J).
    + exfalso. apply (WF_no_loop (x:=z)).
      assert (Z : Stage z) by now apply H. apply XL; auto.
Qed.

Fact not_total_exists :
  ~ total (@Iso M N) -> exists x, Stage x /\ ~ domain x.
Proof.
  intros H. contra H1. apply H.
  intros y. contra H2. apply H1.
  destruct (WF_reachable y) as [z [Z1 Z2]].
  exists z. split; trivial. intros [a I].
  destruct (Iso_btot I Z2) as [b [B1 B2]].
  apply H2. now exists b.
Qed.

Lemma domain_Stage_sub x :
  total (@Iso N M) -> Stage x -> ~ domain x -> domain <=s x.
Proof.
  intros S H I y [a A].
  destruct (WF_reachable a) as [b [B1 B2]].
  destruct (S b) as [z H1].
  assert (H2 : Stage z) by now apply (Iso_Stage H1).
  apply Iso_sym in H1; trivial.
  assert (H3 : y el z) by now apply (Iso_mem H1 A).
  destruct (Stage_lin_el H2 H) as [J|J]; auto.
  contradict I. apply (domain_el (Iso_dom H1) J).
Qed.

Lemma not_total_domain :
  ~ total (@Iso M N) -> total (@Iso N M) -> small (@domain M N).
Proof.
  intros H I. apply not_total_exists in H as [x [X1 X2]].
  apply (bounded_small (domain_Stage_sub I X1 X2)).
Qed.

Fact range_domain x :
  @ domain M N x <-> @ range N M x.
Proof.
  split; intros [a H % Iso_sym]; trivial; now exists a.
Qed.

Fact range_domain_small x :
  agree (@domain M N) x <-> agree (@range N M) x.
Proof.
  split; intros X; intros y; split; intros H.
  - now apply range_domain, X.
  - now apply X, range_domain.
  - now apply range_domain, X.
  - now apply X, range_domain.
Qed.

End Stages.

(* Main results *)

(* We assume two models of ZF for the rest of the development *)

Parameters (M: SetStruct) (MZF : ZF M).
Parameters (N: SetStruct) (NZF : ZF N).

Hint Resolve MZF NZF.

Existing Instance MZF.
Existing Instance NZF.

Implicit Type x y z u : M.
Implicit Type a b c d : N.

Fact Stage_Iso x a :
  least (fun x' => Stage x' /\ ~ (@domain M N) x') x ->
  least (fun a' => Stage a' /\ ~ (@domain N M) a') a ->
  Iso x a.
Proof.
  intros H I. split.
  - apply Stage_btot; trivial; apply I.
  - apply btot_bsur; auto.
    apply Stage_btot; trivial; apply H.
Qed.

Lemma Iso_Stage_max :
  Stage <=p (@domain M N) \/ Stage <=p (@domain N M).
Proof.
  contra H. apply not_or_and in H as [H1 H2].
  apply class_not_sub in H1 as [x[X1 X2]].
  apply class_not_sub in H2 as [a[A1 A2]].
  destruct (Stage_least (p:=fun x => ~ (@domain M N) x) X1 X2) as [y HY].
  destruct (Stage_least (p:=fun a => ~ (@domain N M) a) A1 A2) as [b HB].
  apply HY. exists b. now apply Stage_Iso.
Qed.

Theorem Iso_max :
  total (@Iso M N) \/ surjective (@Iso M N).
Proof.
  contra H. apply not_or_and in H as [H1 H2]. rewrite tot_sur in H2.
  apply not_total_exists in H1 as [x [X1 X2]].
  apply not_total_exists in H2 as [a [A1 A2]].
  destruct (Iso_Stage_max) as [H|H]; auto.
Qed.

Theorem Iso_tricho :
  (total (@Iso M N) /\ surjective (@Iso M N)) \/
  (surjective (@Iso M N) /\ small (@domain M N)) \/
  (total (@Iso M N) /\ small (@range M N)).
Proof.
  destruct (classic (total (@Iso M N))), (classic (surjective (@Iso M N))).
  - now left.
  - right. right. split; trivial. rewrite tot_sur in H0.
    apply not_total_domain in H0 as [x X]; trivial.
    exists x. now apply range_domain_small.
  - right. left. split; trivial.
    rewrite tot_sur in H0. now apply not_total_domain.
  - destruct Iso_max; contradiction.
Qed.

(* To simplify further proofs, we turn the relation Iso into two functions *)

Definition i x := delta (fun a => Iso x a).
Definition j a := delta (fun x => Iso x a).

Fact j_Iso a :
  (@range M N) a -> Iso (j a) a.
Proof.
  intros [x H]. unfold j. eapply delta_spec; eauto.
  hnf. intros. apply (Iso_inj H0 H1).
Qed.

Fact i_Iso x :
  (@domain M N) x -> Iso x (i x).
Proof.
  intros [a H]. unfold i. eapply delta_spec; eauto.
  hnf. intros. apply (Iso_fun H0 H1).
Qed.

Fact ij a :
  (@range M N) a -> i (j a) = a.
Proof.
  intros H. apply delta_eq.
  - hnf. apply Iso_fun.
  - now apply j_Iso.
Qed.

Fact ji x :
  (@domain M N) x -> j (i x) = x.
Proof.
  intros H. apply delta_eq.
  - hnf. intros. eapply Iso_inj; eauto.
  - now apply i_Iso.
Qed.

Fact j_dom a :
  surjective (@Iso M N) -> (@domain M N) (j a).
Proof.
  intros H. exists a. apply j_Iso, H.
Qed.

Fact i_ran x :
  total (@Iso M N) -> (@range M N) (i x).
Proof.
  intros H. exists x. apply i_Iso, H.
Qed.