Require Export Embedding.

(* A Structure is minimal if it contains no universes *)

Definition minimal (M : SetStruct) :=
  ~ exists u : M, universe u.

(* Every model admits a minimal inner model *)

Fact IM_universe p (PC : ZF_closed p) (U : IM NZF PC) :
  universe U -> universe (proj1_sig U).
Proof.
  intros (H1&H2&H3&H4&H5). destruct U as [u PU].
  simpl. repeat split.
  - intros y Y z Z. specialize (H1 (exist p y (p_trans PC Y PU)) Y).
    assert (PZ : p z) by eauto using (p_trans PC).
    now apply (H1 (exist p z PZ)).
  - apply H2.
  - intros y Y. now apply (H3 (exist p y (p_trans PC Y PU))).
  - intros y Y. now apply (H4 (exist p y (p_trans PC Y PU))).
  - intros R x FR UR X.
    assert (FRR : functional (res (p:=p) R)) by now apply res_fun.
    cutrewrite (rep R x = pseudo_rep (res (p:=p) R) x).
    + apply (H5 (res R) (exist p x (p_trans PC X PU))); trivial.
      intros [y PY] [z PZ] RYZ YX. now apply (UR y).
    + rewrite pseudo_rep_fun; trivial.
      apply Ext; intros y [z[Z1 Z2]] % Rep; auto using embed_fun.
      * apply Rep; auto using embed_fun. exists z. split; trivial.
        assert (PZ : p z) by eauto using (p_trans PC).
        assert (PY : p y) by eauto using (p_trans PC).
        exists PZ, PY. exact Z2.
      * apply Rep; trivial. exists z. split; trivial.
        destruct Z2 as [PZ[PY Z2]]. exact Z2.
Qed.

Lemma minimality_cons :
  exists p (PZ : ZF_closed p), ZF (IM NZF PZ) /\ minimal (IM NZF PZ).
Proof.
  destruct (classic (exists u, universe u)) as [[u U]|H].
  - assert (US : Stage u) by now apply universe_stage.
    pattern u in U. destruct (Stage_least US U) as [x[[X1 X2] X3]].
    exists (fun y => y el x). exists (universe_ZF_closed X2).
    split; try apply IM_ZF.
    clear u U US. intros [[u PU] U].
    apply IM_universe in U; simpl in U.
    apply (WF_no_loop (x:=u)). apply X3; auto using universe_stage.
  - exists (fun a => True). assert (I : ZF_closed (fun a => True)) by firstorder.
    exists I. split; try apply IM_ZF; auto. intros [[u PU] U].
    apply IM_universe in U; simpl in U.
    apply H. now exists u.
Qed.

(* ZF plus minimality is categorical *)

Theorem Iso_bijective_minimal :
  minimal M -> minimal N -> total (@Iso M N) /\ surjective (@Iso M N).
Proof.
  intros Min1 Min2.
  destruct Iso_tricho as [H|[[IS[X HX]]|[IT[A HA]]]]; trivial.
  - exfalso. apply Min1. exists X.
    now apply domain_universe.
  - exfalso. apply Min2. exists A.
    apply range_domain_small in HA.
    now apply (domain_universe (N:=M)).
Qed.