Section Categoricity.
Context { M : ZFStruct }.
Context { MZF : ZF M }.
Context { N : ZFStruct }.
Context { NZF : ZF N }.
(* Suppose M and N are equipotent models *)
Variable F : M -> N.
Variable G : N -> M.
Variable FG : forall a, F (G a) = a.
Variable GF : forall x, G (F x) = x.
(* Then Iso must be both total and surjective, hence M N are isomorphic *)
Theorem cat_card :
iso M N.
Proof.
destruct (@Iso_tricho M MZF N NZF) as [H|[[IS[X HX]]|[IT[A HA]]]]; trivial.
- exfalso. pose (Y := sep (fun x => x nel G (i x)) X). pose (y := @j M N (F Y)).
specialize (sep_el (fun x => x nel G (i x)) X y). intros H. fold Y in H.
unfold y in H at 3. rewrite ij, GF in H; try apply IS.
assert (I : y el X) by now apply HX, j_dom. tauto.
- exfalso. pose (B := sep (fun a => a nel F (j a)) A). pose (b := i (G B)).
specialize (sep_el (fun a => a nel F (j a)) A b). intros H. fold B in H.
unfold b in H at 3. rewrite ji, FG in H; try apply IT.
assert (I : b el A) by now apply HA, i_ran. tauto.
Qed.
End Categoricity.
Lemma cat_ZFn (M N : ZFStruct) n :
ZFn n M -> ZFn n N -> iso M N.
Proof.
intros [[MZF M1] M2] [[NZF N1] N2].
destruct (@Iso_tricho M MZF N NZF) as [H|[[IS[X HX]]|[IT[A HA]]]]; trivial.
- exfalso. apply M2. exists (power X); simpl.
assert (XU : universe X) by now apply domain_universe.
exists X. split; try apply power_eager. split; trivial.
apply trans_strength; try now apply universe_trans.
destruct N1 as [a N1]. exists (j a).
split; try now apply HX, j_dom.
apply (Iso_strength N1), Iso_sym, j_Iso, IS; trivial.
- exfalso. apply N2. exists (power A); simpl.
apply range_domain_small in HA. apply tot_sur in IT.
assert (XU : universe A) by now apply (domain_universe (N:=M)).
exists A. split; try apply power_eager. split; trivial.
apply trans_strength; try now apply universe_trans.
destruct M1 as [x M1]. exists (j x).
split; try now apply HA, j_dom.
apply (Iso_strength M1), Iso_sym, j_Iso, IT; trivial.
Qed.