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.