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 : a, F (G a) = a.
  Variable GF : 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 ! ( x x G (i x))). pose (y := j (F Y)).
      specialize (sep_el X ( x x 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 X) by now apply HX, j_dom. tauto.
    - exfalso. pose (B := A ! ( a a F (j a))). pose (b := i (G B)).
      specialize (sep_el A ( a a 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 A) by now apply HA, i_ran. tauto.
  Qed.


End Categoricity.