Require Export Embedding.

(* We define a predicate stating that a set contains n universes *)

Fixpoint Un n (M : SetStruct) (x : M) :=
  match n with
    | O => True
    | S n => exists u, u el x /\ universe u /\ (Un n u)
  end.

Fact Iso_Un n (M N : SetStruct) {MZF : ZF M} {NZF : ZF N} (x : M) (a : N) :
  Iso x a -> Un n x -> Un n a.
Proof.
  revert x a. induction n; simpl; intros x a H1; auto.
  intros [y[Y1[Y2 Y3]]].
  destruct (Iso_btot H1 Y1) as [b[B1 B2]].
  exists b. split; trivial. split; try now apply (IHn y).
  now apply (Iso_universe B2).
Qed.

(* ZF_n+1 is expressed by the following *)

Definition unis n (M : SetStruct) :=
  (exists u, universe u /\ @Un n M u) /\ (~ exists u, universe u /\ @Un (S n) M u).

(* ZF_n+1 is categorical *)

Theorem Iso_bijective_ZFn n :
  unis n M -> unis n N -> total (@Iso M N) /\ surjective (@Iso M N).
Proof.
  intros MZFn NZFn.
  destruct (Iso_tricho) as [H|[[IS[X HX]]|[IT[A HA]]]]; trivial.
  - exfalso. apply MZFn. exists X; simpl.
    destruct NZFn as [[u[H1 H2]] _].
    split. now apply domain_universe. exists (j u).
    split. apply HX. now apply j_dom. split.
    + apply (Iso_universe (x:=u)); trivial.
      apply Iso_sym, j_Iso; trivial. apply IS.
    + apply (Iso_Un (x:=u)); trivial.
      apply Iso_sym, j_Iso; trivial. apply IS.
  - exfalso. apply NZFn. exists A; simpl.
    destruct MZFn as [[u[H1 H2]] _].
    split. apply range_domain_small in HA.
    now apply (domain_universe (N:=M)). exists (i u).
    split. apply HA. now apply i_ran. split.
    + apply (Iso_universe (x:=u)); trivial.
      apply i_Iso; trivial. apply IT.
    + apply (Iso_Un (x:=u)); trivial.
      apply i_Iso; trivial. apply IT.
Qed.