# Categoricity in Every Cardinality

Require Export Embedding.

Section Categoricity.

(* 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 Iso_bijective_equipotent :
total (@Iso M N) /\ surjective (@Iso M N).
Proof.
destruct (Iso_tricho) as [H|[[IS[X HX]]|[IT[A HA]]]]; trivial.
- exfalso. pose (Y := X ! (fun x => x nel G (i x))). pose (y := j (F Y)).
specialize (sep_el X (fun x => x nel G (i 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 := A ! (fun a => a nel F (j a))). pose (b := i (G B)).
specialize (sep_el A (fun a => a nel F (j 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.