# Categoricity of ZFn for n > 0

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.