Library ZFgrothendieck

Require Import ZF.
Require Import ZFpairs ZFsum ZFrelations ZFrepl ZFwf ZFord ZFfix.
Require Import ZFstable.
Require Import ZFlist.

Record grot_univ (U:set) : Prop := {
  G_trans : ∀ x y, y ∈ x -> x ∈ U -> y ∈ U;
  G_pair : ∀ x y, x ∈ U -> y ∈ U -> pair x y ∈ U;
  G_power : ∀ x, x ∈ U -> power x ∈ U;
  G_union_repl : ∀ I R, repl_rel I R -> I ∈ U ->
                (∀ x y, x ∈ I -> R x y -> y ∈ U) ->
                union (repl I R) ∈ U }.

Lemma grot_univ_ext : ∀ U U',
  U == U' -> grot_univ U -> grot_univ U'.

Lemma grot_empty : grot_univ empty.


Section GrothendieckUniverse.

Variable U : set.
Hypothesis grot : grot_univ U.

Lemma G_incl : ∀ x y, x ∈ U -> y ⊆ x -> y ∈ U.

Lemma G_subset : ∀ x P, x ∈ U -> subset x P ∈ U.

Lemma G_singl : ∀ x, x ∈ U -> singl x ∈ U.

Lemma G_repl : ∀ A R,
  repl_rel A R ->
  A ∈ U ->
  (∀ x y, x ∈ A -> R x y -> y ∈ U) ->
  repl A R ∈ U.

Lemma G_union : ∀ x, x ∈ U -> union x ∈ U.

Lemma G_replf : ∀ A F,
  ext_fun A F ->
  A ∈ U ->
  (∀ x, x ∈ A -> F x ∈ U) ->
  replf A F ∈ U.

Lemma G_union2 : ∀ x y, x ∈ U -> y ∈ U -> x ∪ y ∈ U.

Lemma G_sup A B :
  ext_fun A B ->
  A ∈ U ->
  (∀ x, x ∈ A -> B x ∈ U) ->
  sup A B ∈ U.

Lemma G_nat x : x ∈ U -> ZFnats.N ⊆ U.

Lemma G_prodcart : ∀ A B, A ∈ U -> B ∈ U -> prodcart A B ∈ U.

Lemma G_couple : ∀ x y, x ∈ U -> y ∈ U -> couple x y ∈ U.

  Lemma G_sum X Y : X ∈ U -> Y ∈ U -> sum X Y ∈ U.

Lemma G_sumcase A B f g a :
  morph1 f ->
  morph1 g ->
  a ∈ sum A B ->
  (∀ a, a ∈ A -> f a ∈ U) ->
  (∀ a, a ∈ B -> g a ∈ U) ->
  sum_case f g a ∈ U.

Lemma G_rel : ∀ A B, A ∈ U -> B ∈ U -> rel A B ∈ U.

Lemma G_func : ∀ A B, A ∈ U -> B ∈ U -> func A B ∈ U.

Lemma G_dep_func : ∀ X Y,
  ext_fun X Y ->
  X ∈ U ->
  (∀ x, x ∈ X -> Y x ∈ U) ->
  dep_func X Y ∈ U.

Lemma G_app f x :
  f ∈ U -> x ∈ U -> app f x ∈ U.

  Lemma G_sigma A B :
    ext_fun A B ->
    A ∈ U ->
    (∀ x, x ∈ A -> B x ∈ U) ->
    sigma A B ∈ U.

  Lemma G_cc_lam A F :
    ext_fun A F ->
    A ∈ U ->
    (∀ x, x ∈ A -> F x ∈ U) ->
    cc_lam A F ∈ U.

  Lemma G_cc_app f x :
    f ∈ U -> x ∈ U -> cc_app f x ∈ U.

  Lemma G_cc_prod A B :
    ext_fun A B ->
    A ∈ U ->
    (∀ x, x ∈ A -> B x ∈ U) ->
    cc_prod A B ∈ U.

  Lemma G_TR F o :
    Proper ((eq_set==>eq_set)==>eq_set==>eq_set) F ->
    (∀ o f f', isOrd o -> eq_fun o f f' -> F f o == F f' o) ->
    isOrd o ->
    o ∈ U ->
    (∀ f o, ext_fun o f -> o ∈ U ->
     (∀ o', o' ∈ o -> f o' ∈ U) ->
     F f o ∈ U) ->
    TR F o ∈ U.

  Lemma G_TI F o :
    morph1 F ->
    isOrd o ->
    o ∈ U ->
    (∀ x, x ∈ U -> F x ∈ U) ->
    TI F o ∈ U.

Lemma G_osup2 x y :
  isWf x -> x ∈ U -> y ∈ U -> x ⊔ y ∈ U.

  Lemma G_Ffix F A : A ∈ U -> Ffix F A ∈ U.

Section NonTrivial.

  Hypothesis Unontriv : empty ∈ U.

End NonTrivial.

Section Infinite.

  Hypothesis Uinf : omega ∈ U.

  Lemma G_inf_nontriv : empty ∈ U.
  Hint Resolve G_inf_nontriv.

  Lemma G_List A : A ∈ U -> List A ∈ U.

  Lemma G_N : ZFnats.N ∈ U.

Lemma G_osup I f :
  ext_fun I f ->
  (∀ x, x ∈ I -> isOrd (f x)) ->
  I ∈ U ->
  (∀ x, x ∈ I -> f x ∈ U) ->
  osup I f ∈ U.

  Lemma G_Ffix_ord F A :
    Proper (incl_set ==> incl_set) F ->
    (∀ X, X ⊆ A -> F X ⊆ A) ->
    A ∈ U ->
    Ffix_ord F A ∈ U.

End Infinite.


End GrothendieckUniverse.

Lemma grot_inter : ∀ UU,
  (exists x, x ∈ UU) ->
  (∀ x, x ∈ UU -> grot_univ x) ->
  grot_univ (inter UU).

Lemma grot_intersection : ∀ (P:set->Prop) x,
  grot_univ x -> P x ->
  grot_univ (subset x (fun y => ∀ U, grot_univ U -> P U -> y ∈ U)).

Definition grot_succ_pred x y :=
  grot_univ y /\ x ∈ y /\ ∀ U, grot_univ U -> x ∈ U -> y ⊆ U.

Definition grothendieck := ∀ x, exists2 U, grot_univ U & x ∈ U.

Section TarskiGrothendieck.

Variable gr : grothendieck.

Lemma grot_inter_unique : ∀ x, uchoice_pred (grot_succ_pred x).

Definition grot_succ U := uchoice (grot_succ_pred U).

Lemma grot_succ_typ : ∀ x, grot_univ (grot_succ x).

Lemma grot_succ_in : ∀ x, x ∈ grot_succ x.

End TarskiGrothendieck.